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 syl5bb 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