Metamath Proof Explorer

Theorem r0cld

Description: The analogue of the T_1 axiom (singletons are closed) for an R_0 space. In an R_0 space the set of all points topologically indistinguishable from A is closed. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis kqval.2 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
Assertion r0cld ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → z ∈ X | ∀ o ∈ J z ∈ o ↔ A ∈ o ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 kqval.2 ⊢ F = x ∈ X ⟼ y ∈ J | x ∈ y
2 1 kqffn ⊢ J ∈ TopOn ⁡ X → F Fn X
3 2 3ad2ant1 ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → F Fn X
4 fncnvima2 ⊢ F Fn X → F -1 F ⁡ A = z ∈ X | F ⁡ z ∈ F ⁡ A
5 3 4 syl ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → F -1 F ⁡ A = z ∈ X | F ⁡ z ∈ F ⁡ A
6 fvex ⊢ F ⁡ z ∈ V
7 6 elsn ⊢ F ⁡ z ∈ F ⁡ A ↔ F ⁡ z = F ⁡ A
8 simpl1 ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X ∧ z ∈ X → J ∈ TopOn ⁡ X
9 simpr ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X ∧ z ∈ X → z ∈ X
10 simpl3 ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X ∧ z ∈ X → A ∈ X
11 1 kqfeq ⊢ J ∈ TopOn ⁡ X ∧ z ∈ X ∧ A ∈ X → F ⁡ z = F ⁡ A ↔ ∀ y ∈ J z ∈ y ↔ A ∈ y
12 eleq2w ⊢ y = o → z ∈ y ↔ z ∈ o
13 eleq2w ⊢ y = o → A ∈ y ↔ A ∈ o
14 12 13 bibi12d ⊢ y = o → z ∈ y ↔ A ∈ y ↔ z ∈ o ↔ A ∈ o
15 14 cbvralvw ⊢ ∀ y ∈ J z ∈ y ↔ A ∈ y ↔ ∀ o ∈ J z ∈ o ↔ A ∈ o
16 11 15 bitrdi ⊢ J ∈ TopOn ⁡ X ∧ z ∈ X ∧ A ∈ X → F ⁡ z = F ⁡ A ↔ ∀ o ∈ J z ∈ o ↔ A ∈ o
17 8 9 10 16 syl3anc ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X ∧ z ∈ X → F ⁡ z = F ⁡ A ↔ ∀ o ∈ J z ∈ o ↔ A ∈ o
18 7 17 bitrid ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X ∧ z ∈ X → F ⁡ z ∈ F ⁡ A ↔ ∀ o ∈ J z ∈ o ↔ A ∈ o
19 18 rabbidva ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → z ∈ X | F ⁡ z ∈ F ⁡ A = z ∈ X | ∀ o ∈ J z ∈ o ↔ A ∈ o
20 5 19 eqtrd ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → F -1 F ⁡ A = z ∈ X | ∀ o ∈ J z ∈ o ↔ A ∈ o
21 1 kqid ⊢ J ∈ TopOn ⁡ X → F ∈ J Cn KQ ⁡ J
22 21 3ad2ant1 ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → F ∈ J Cn KQ ⁡ J
23 simp2 ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → KQ ⁡ J ∈ Fre
24 simp3 ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → A ∈ X
25 fnfvelrn ⊢ F Fn X ∧ A ∈ X → F ⁡ A ∈ ran ⁡ F
26 3 24 25 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → F ⁡ A ∈ ran ⁡ F
27 1 kqtopon ⊢ J ∈ TopOn ⁡ X → KQ ⁡ J ∈ TopOn ⁡ ran ⁡ F
28 27 3ad2ant1 ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → KQ ⁡ J ∈ TopOn ⁡ ran ⁡ F
29 toponuni ⊢ KQ ⁡ J ∈ TopOn ⁡ ran ⁡ F → ran ⁡ F = ⋃ KQ ⁡ J
30 28 29 syl ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → ran ⁡ F = ⋃ KQ ⁡ J
31 26 30 eleqtrd ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → F ⁡ A ∈ ⋃ KQ ⁡ J
32 eqid ⊢ ⋃ KQ ⁡ J = ⋃ KQ ⁡ J
33 32 t1sncld ⊢ KQ ⁡ J ∈ Fre ∧ F ⁡ A ∈ ⋃ KQ ⁡ J → F ⁡ A ∈ Clsd ⁡ KQ ⁡ J
34 23 31 33 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → F ⁡ A ∈ Clsd ⁡ KQ ⁡ J
35 cnclima ⊢ F ∈ J Cn KQ ⁡ J ∧ F ⁡ A ∈ Clsd ⁡ KQ ⁡ J → F -1 F ⁡ A ∈ Clsd ⁡ J
36 22 34 35 syl2anc ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → F -1 F ⁡ A ∈ Clsd ⁡ J
37 20 36 eqeltrrd ⊢ J ∈ TopOn ⁡ X ∧ KQ ⁡ J ∈ Fre ∧ A ∈ X → z ∈ X | ∀ o ∈ J z ∈ o ↔ A ∈ o ∈ Clsd ⁡ J