[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set α
h : IsOpen s
⊢ ∀ (t : Set α), t ∈ {s} → IsOpen t
[PROOFSTEP]
simp [h]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
I : Set ι
hI : Set.Countable I
f : ι → Set α
hf : ∀ (i : ι), i ∈ I → IsOpen (f i)
⊢ ∀ (t : Set α), t ∈ f '' I → IsOpen t
[PROOFSTEP]
rwa [ball_image_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
I : Set ι
hI : Set.Countable I
f : ι → Set α
hf : ∀ (i : ι), i ∈ I → IsOpen (f i)
⊢ ⋂ (i : ι) (_ : i ∈ I), f i = ⋂₀ (f '' I)
[PROOFSTEP]
rw [sInter_image]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
f : ι → Set α
hf : ∀ (i : ι), IsOpen (f i)
⊢ ∀ (t : Set α), t ∈ range f → IsOpen t
[PROOFSTEP]
rwa [forall_range_iff]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
f : ι → Set α
hf : ∀ (i : ι), IsOpen (f i)
⊢ ⋂ (i : ι), f i = ⋂₀ range f
[PROOFSTEP]
rw [sInter_range]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
s : ι → Set α
hs : ∀ (i : ι), IsGδ (s i)
⊢ IsGδ (⋂ (i : ι), s i)
[PROOFSTEP]
choose T hTo hTc hTs using hs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
s : ι → Set α
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), s i = ⋂₀ T i
⊢ IsGδ (⋂ (i : ι), s i)
[PROOFSTEP]
obtain rfl : s = fun i => ⋂₀ T i := funext hTs
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ IsGδ (⋂ (i : ι), (fun i => ⋂₀ T i) i)
[PROOFSTEP]
refine' ⟨⋃ i, T i, _, countable_iUnion hTc, (sInter_iUnion _).symm⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : Encodable ι
T : ι → Set (Set α)
hTo : ∀ (i : ι) (t : Set α), t ∈ T i → IsOpen t
hTc : ∀ (i : ι), Set.Countable (T i)
hTs : ∀ (i : ι), (fun i => ⋂₀ T i) i = ⋂₀ T i
⊢ ∀ (t : Set α), t ∈ ⋃ (i : ι), T i → IsOpen t
[PROOFSTEP]
simpa [@forall_swap ι] using hTo
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Countable s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ (i : ι) (h : i ∈ s), t i h)
[PROOFSTEP]
rw [biInter_eq_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Countable s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
⊢ IsGδ (⋂ (x : ↑s), t ↑x (_ : ↑x ∈ s))
[PROOFSTEP]
haveI := hs.toEncodable
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Countable s
t : (i : ι) → i ∈ s → Set α
ht : ∀ (i : ι) (hi : i ∈ s), IsGδ (t i hi)
this : Encodable ↑s
⊢ IsGδ (⋂ (x : ↑s), t ↑x (_ : ↑x ∈ s))
[PROOFSTEP]
exact isGδ_iInter fun x => ht x x.2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
S : Set (Set α)
h : ∀ (s : Set α), s ∈ S → IsGδ s
hS : Set.Countable S
⊢ IsGδ (⋂₀ S)
[PROOFSTEP]
simpa only [sInter_eq_biInter] using isGδ_biInter hS h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∩ t)
[PROOFSTEP]
rw [inter_eq_iInter]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (⋂ (b : Bool), bif b then s else t)
[PROOFSTEP]
exact isGδ_iInter (Bool.forall_bool.2 ⟨ht, hs⟩)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s t : Set α
hs : IsGδ s
ht : IsGδ t
⊢ IsGδ (s ∪ t)
[PROOFSTEP]
rcases hs with ⟨S, Sopen, Scount, rfl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
t : Set α
ht : IsGδ t
S : Set (Set α)
Sopen : ∀ (t : Set α), t ∈ S → IsOpen t
Scount : Set.Countable S
⊢ IsGδ (⋂₀ S ∪ t)
[PROOFSTEP]
rcases ht with ⟨T, Topen, Tcount, rfl⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
S : Set (Set α)
Sopen : ∀ (t : Set α), t ∈ S → IsOpen t
Scount : Set.Countable S
T : Set (Set α)
Topen : ∀ (t : Set α), t ∈ T → IsOpen t
Tcount : Set.Countable T
⊢ IsGδ (⋂₀ S ∪ ⋂₀ T)
[PROOFSTEP]
rw [sInter_union_sInter]
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
S : Set (Set α)
Sopen : ∀ (t : Set α), t ∈ S → IsOpen t
Scount : Set.Countable S
T : Set (Set α)
Topen : ∀ (t : Set α), t ∈ T → IsOpen t
Tcount : Set.Countable T
⊢ IsGδ (⋂ (p : Set α × Set α) (_ : p ∈ S ×ˢ T), p.fst ∪ p.snd)
[PROOFSTEP]
apply isGδ_biInter_of_open (Scount.prod Tcount)
[GOAL]
case intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
S : Set (Set α)
Sopen : ∀ (t : Set α), t ∈ S → IsOpen t
Scount : Set.Countable S
T : Set (Set α)
Topen : ∀ (t : Set α), t ∈ T → IsOpen t
Tcount : Set.Countable T
⊢ ∀ (i : Set α × Set α), i ∈ S ×ˢ T → IsOpen (i.fst ∪ i.snd)
[PROOFSTEP]
rintro ⟨a, b⟩ ⟨ha, hb⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.mk.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
S : Set (Set α)
Sopen : ∀ (t : Set α), t ∈ S → IsOpen t
Scount : Set.Countable S
T : Set (Set α)
Topen : ∀ (t : Set α), t ∈ T → IsOpen t
Tcount : Set.Countable T
a b : Set α
ha : (a, b).fst ∈ S
hb : (a, b).snd ∈ T
⊢ IsOpen ((a, b).fst ∪ (a, b).snd)
[PROOFSTEP]
exact (Sopen a ha).union (Topen b hb)
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ IsGδ (⋃ (i : ι) (_ : i ∈ s), f i)
[PROOFSTEP]
refine' Finite.induction_on hs (by simp) _ h
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ (∀ (i : ι), i ∈ ∅ → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ ∅), f i)
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ ∀ {a : ι} {s : Set ι},
    ¬a ∈ s →
      Set.Finite s →
        ((∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ s), f i)) →
          (∀ (i : ι), i ∈ insert a s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ insert a s), f i)
[PROOFSTEP]
simp only [ball_insert_iff, biUnion_insert]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set ι
hs : Set.Finite s
f : ι → Set α
h : ∀ (i : ι), i ∈ s → IsGδ (f i)
⊢ ∀ {a : ι} {s : Set ι},
    ¬a ∈ s →
      Set.Finite s →
        ((∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (⋃ (i : ι) (_ : i ∈ s), f i)) →
          (IsGδ (f a) ∧ ∀ (i : ι), i ∈ s → IsGδ (f i)) → IsGδ (f a ∪ ⋃ (i : ι) (_ : i ∈ s), f i)
[PROOFSTEP]
exact fun _ _ ihs H => H.1.union (ihs H.2)
[GOAL]
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α✝
α : Type u_5
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
⊢ IsGδ s
[PROOFSTEP]
rcases(@uniformity_hasBasis_open α _).exists_antitone_subbasis with ⟨U, hUo, hU, -⟩
[GOAL]
case intro.intro.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α✝
α : Type u_5
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
⊢ IsGδ s
[PROOFSTEP]
rw [← hs.closure_eq, ← hU.biInter_biUnion_ball]
[GOAL]
case intro.intro.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α✝
α : Type u_5
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
⊢ IsGδ (⋂ (i : ℕ) (_ : True), ⋃ (x : α) (_ : x ∈ s), UniformSpace.ball x (id (U i)))
[PROOFSTEP]
refine' isGδ_biInter (to_countable _) fun n _ => IsOpen.isGδ _
[GOAL]
case intro.intro.mk
α✝ : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α✝
α : Type u_5
inst✝¹ : UniformSpace α
inst✝ : IsCountablyGenerated (uniformity α)
s : Set α
hs : IsClosed s
U : ℕ → Set (α × α)
hUo : ∀ (i : ℕ), U i ∈ uniformity α ∧ IsOpen (U i)
hU : HasBasis (uniformity α) (fun x => True) fun i => id (U i)
n : ℕ
x✝ : n ∈ fun i => True
⊢ IsOpen (⋃ (x : α) (_ : x ∈ s), UniformSpace.ball x (id (U n)))
[PROOFSTEP]
exact isOpen_biUnion fun x _ => UniformSpace.isOpen_ball _ (hUo _).2
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
hs : Set.Countable s
⊢ IsGδ sᶜ
[PROOFSTEP]
rw [← biUnion_of_singleton s, compl_iUnion₂]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝¹ : TopologicalSpace α
inst✝ : T1Space α
s : Set α
hs : Set.Countable s
⊢ IsGδ (⋂ (i : α) (_ : i ∈ s), {i}ᶜ)
[PROOFSTEP]
exact isGδ_biInter hs fun x _ => isGδ_compl_singleton x
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : FirstCountableTopology α
a : α
⊢ IsGδ {a}
[PROOFSTEP]
rcases(nhds_basis_opens a).exists_antitone_subbasis with ⟨U, hU, h_basis⟩
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : FirstCountableTopology α
a : α
U : ℕ → Set α
hU : ∀ (i : ℕ), a ∈ U i ∧ IsOpen (U i)
h_basis : HasAntitoneBasis (𝓝 a) fun i => U i
⊢ IsGδ {a}
[PROOFSTEP]
rw [← biInter_basis_nhds h_basis.toHasBasis]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : T1Space α
inst✝ : FirstCountableTopology α
a : α
U : ℕ → Set α
hU : ∀ (i : ℕ), a ∈ U i ∧ IsOpen (U i)
h_basis : HasAntitoneBasis (𝓝 a) fun i => U i
⊢ IsGδ (⋂ (i : ℕ) (_ : True), U i)
[PROOFSTEP]
exact isGδ_biInter (to_countable _) fun n _ => (hU n).2.isGδ
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
⊢ IsGδ {x | ContinuousAt f x}
[PROOFSTEP]
obtain ⟨U, _, hU⟩ := (@uniformity_hasBasis_open_symmetric β _).exists_antitone_subbasis
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ {x | ContinuousAt f x}
[PROOFSTEP]
simp only [Uniform.continuousAt_iff_prod, nhds_prod_eq]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ {x | Tendsto (fun x => (f x.fst, f x.snd)) (𝓝 x ×ˢ 𝓝 x) (uniformity β)}
[PROOFSTEP]
simp only [(nhds_basis_opens _).prod_self.tendsto_iff hU.toHasBasis, forall_prop_of_true, setOf_forall, id]
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
⊢ IsGδ (⋂ (i : ℕ), {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U i})
[PROOFSTEP]
refine' isGδ_iInter fun k => IsOpen.isGδ <| isOpen_iff_mem_nhds.2 fun x => _
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
k : ℕ
x : α
⊢ x ∈ {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} →
    {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} ∈ 𝓝 x
[PROOFSTEP]
rintro ⟨s, ⟨hsx, hso⟩, hsU⟩
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝² : TopologicalSpace α
inst✝¹ : UniformSpace β
inst✝ : IsCountablyGenerated (uniformity β)
f : α → β
U : ℕ → Set (β × β)
left✝ : ∀ (i : ℕ), U i ∈ uniformity β ∧ IsOpen (U i) ∧ SymmetricRel (U i)
hU : HasAntitoneBasis (uniformity β) fun i => id (U i)
k : ℕ
x : α
s : Set α
hsU : ∀ (x : α × α), x ∈ s ×ˢ s → (f x.fst, f x.snd) ∈ U k
hsx : x ∈ s
hso : IsOpen s
⊢ {x | ∃ ia, (x ∈ ia ∧ IsOpen ia) ∧ ∀ (x : α × α), x ∈ ia ×ˢ ia → (f x.fst, f x.snd) ∈ U k} ∈ 𝓝 x
[PROOFSTEP]
filter_upwards [IsOpen.mem_nhds hso hsx] with _ hy using ⟨s, ⟨hy, hso⟩, hsU⟩
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
⊢ CountableInterFilter (residual α)
[PROOFSTEP]
rw [residual]
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
⊢ CountableInterFilter (countableGenerate {t | IsOpen t ∧ Dense t})
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set α
ho : IsGδ s
hd : Dense s
⊢ s ∈ residual α
[PROOFSTEP]
rcases ho with ⟨T, To, Tct, rfl⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
T : Set (Set α)
To : ∀ (t : Set α), t ∈ T → IsOpen t
Tct : Set.Countable T
hd : Dense (⋂₀ T)
⊢ ⋂₀ T ∈ residual α
[PROOFSTEP]
exact (countable_sInter_mem Tct).mpr fun t tT => residual_of_dense_open (To t tT) (hd.mono (sInter_subset_of_mem tT))
[GOAL]
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
inst✝ : TopologicalSpace α
s : Set α
⊢ (∃ S, S ⊆ {t | IsOpen t ∧ Dense t} ∧ Set.Countable S ∧ ⋂₀ S ⊆ s) ↔
    ∃ S, (∀ (t : Set α), t ∈ S → IsOpen t) ∧ (∀ (t : Set α), t ∈ S → Dense t) ∧ Set.Countable S ∧ ⋂₀ S ⊆ s
[PROOFSTEP]
simp_rw [subset_def, mem_setOf, forall_and, and_assoc]
