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∈Jz∈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→FFnX
3 2 3ad2ant1 ⊢J∈TopOn⁡X∧KQ⁡J∈Fre∧A∈X→FFnX
4 fncnvima2 ⊢FFnX→F-1F⁡A=z∈X|F⁡z∈F⁡A
5 3 4 syl ⊢J∈TopOn⁡X∧KQ⁡J∈Fre∧A∈X→F-1F⁡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∈Jz∈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∈Jz∈y↔A∈y↔∀o∈Jz∈o↔A∈o
16 11 15 bitrdi ⊢J∈TopOn⁡X∧z∈X∧A∈X→F⁡z=F⁡A↔∀o∈Jz∈o↔A∈o
17 8 9 10 16 syl3anc ⊢J∈TopOn⁡X∧KQ⁡J∈Fre∧A∈X∧z∈X→F⁡z=F⁡A↔∀o∈Jz∈o↔A∈o
18 7 17 bitrid ⊢J∈TopOn⁡X∧KQ⁡J∈Fre∧A∈X∧z∈X→F⁡z∈F⁡A↔∀o∈Jz∈o↔A∈o
19 18 rabbidva ⊢J∈TopOn⁡X∧KQ⁡J∈Fre∧A∈X→z∈X|F⁡z∈F⁡A=z∈X|∀o∈Jz∈o↔A∈o
20 5 19 eqtrd ⊢J∈TopOn⁡X∧KQ⁡J∈Fre∧A∈X→F-1F⁡A=z∈X|∀o∈Jz∈o↔A∈o
21 1 kqid ⊢J∈TopOn⁡X→F∈JCnKQ⁡J
22 21 3ad2ant1 ⊢J∈TopOn⁡X∧KQ⁡J∈Fre∧A∈X→F∈JCnKQ⁡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 ⊢FFnX∧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∈JCnKQ⁡J∧F⁡A∈Clsd⁡KQ⁡J→F-1F⁡A∈Clsd⁡J
36 22 34 35 syl2anc ⊢J∈TopOn⁡X∧KQ⁡J∈Fre∧A∈X→F-1F⁡A∈Clsd⁡J
37 20 36 eqeltrrd ⊢J∈TopOn⁡X∧KQ⁡J∈Fre∧A∈X→z∈X|∀o∈Jz∈o↔A∈o∈Clsd⁡J