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 e. X |-> { y e. J | x e. y } )
Assertion r0cld 
|- ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> { z e. X | A. o e. J ( z e. o <-> A e. o ) } e. ( Clsd ` J ) )

Proof

Step Hyp Ref Expression
1 kqval.2 
 |-  F = ( x e. X |-> { y e. J | x e. y } )
2 1 kqffn 
 |-  ( J e. ( TopOn ` X ) -> F Fn X )
3 2 3ad2ant1 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> F Fn X )
4 fncnvima2 
 |-  ( F Fn X -> ( `' F " { ( F ` A ) } ) = { z e. X | ( F ` z ) e. { ( F ` A ) } } )
5 3 4 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> ( `' F " { ( F ` A ) } ) = { z e. X | ( F ` z ) e. { ( F ` A ) } } )
6 fvex 
 |-  ( F ` z ) e. _V
7 6 elsn 
 |-  ( ( F ` z ) e. { ( F ` A ) } <-> ( F ` z ) = ( F ` A ) )
8 simpl1 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) /\ z e. X ) -> J e. ( TopOn ` X ) )
9 simpr 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) /\ z e. X ) -> z e. X )
10 simpl3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) /\ z e. X ) -> A e. X )
11 1 kqfeq 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. X /\ A e. X ) -> ( ( F ` z ) = ( F ` A ) <-> A. y e. J ( z e. y <-> A e. y ) ) )
12 eleq2w 
 |-  ( y = o -> ( z e. y <-> z e. o ) )
13 eleq2w 
 |-  ( y = o -> ( A e. y <-> A e. o ) )
14 12 13 bibi12d 
 |-  ( y = o -> ( ( z e. y <-> A e. y ) <-> ( z e. o <-> A e. o ) ) )
15 14 cbvralvw 
 |-  ( A. y e. J ( z e. y <-> A e. y ) <-> A. o e. J ( z e. o <-> A e. o ) )
16 11 15 bitrdi 
 |-  ( ( J e. ( TopOn ` X ) /\ z e. X /\ A e. X ) -> ( ( F ` z ) = ( F ` A ) <-> A. o e. J ( z e. o <-> A e. o ) ) )
17 8 9 10 16 syl3anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) /\ z e. X ) -> ( ( F ` z ) = ( F ` A ) <-> A. o e. J ( z e. o <-> A e. o ) ) )
18 7 17 syl5bb 
 |-  ( ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) /\ z e. X ) -> ( ( F ` z ) e. { ( F ` A ) } <-> A. o e. J ( z e. o <-> A e. o ) ) )
19 18 rabbidva 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> { z e. X | ( F ` z ) e. { ( F ` A ) } } = { z e. X | A. o e. J ( z e. o <-> A e. o ) } )
20 5 19 eqtrd 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> ( `' F " { ( F ` A ) } ) = { z e. X | A. o e. J ( z e. o <-> A e. o ) } )
21 1 kqid 
 |-  ( J e. ( TopOn ` X ) -> F e. ( J Cn ( KQ ` J ) ) )
22 21 3ad2ant1 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> F e. ( J Cn ( KQ ` J ) ) )
23 simp2 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> ( KQ ` J ) e. Fre )
24 simp3 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> A e. X )
25 fnfvelrn 
 |-  ( ( F Fn X /\ A e. X ) -> ( F ` A ) e. ran F )
26 3 24 25 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> ( F ` A ) e. ran F )
27 1 kqtopon 
 |-  ( J e. ( TopOn ` X ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )
28 27 3ad2ant1 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> ( KQ ` J ) e. ( TopOn ` ran F ) )
29 toponuni 
 |-  ( ( KQ ` J ) e. ( TopOn ` ran F ) -> ran F = U. ( KQ ` J ) )
30 28 29 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> ran F = U. ( KQ ` J ) )
31 26 30 eleqtrd 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> ( F ` A ) e. U. ( KQ ` J ) )
32 eqid 
 |-  U. ( KQ ` J ) = U. ( KQ ` J )
33 32 t1sncld 
 |-  ( ( ( KQ ` J ) e. Fre /\ ( F ` A ) e. U. ( KQ ` J ) ) -> { ( F ` A ) } e. ( Clsd ` ( KQ ` J ) ) )
34 23 31 33 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> { ( F ` A ) } e. ( Clsd ` ( KQ ` J ) ) )
35 cnclima 
 |-  ( ( F e. ( J Cn ( KQ ` J ) ) /\ { ( F ` A ) } e. ( Clsd ` ( KQ ` J ) ) ) -> ( `' F " { ( F ` A ) } ) e. ( Clsd ` J ) )
36 22 34 35 syl2anc 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> ( `' F " { ( F ` A ) } ) e. ( Clsd ` J ) )
37 20 36 eqeltrrd 
 |-  ( ( J e. ( TopOn ` X ) /\ ( KQ ` J ) e. Fre /\ A e. X ) -> { z e. X | A. o e. J ( z e. o <-> A e. o ) } e. ( Clsd ` J ) )