Metamath Proof Explorer

Theorem isreg2

Description: A topological space is regular if any closed set is separated from any point not in it by neighborhoods. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion isreg2 
|- ( J e. ( TopOn ` X ) -> ( J e. Reg <-> A. c e. ( Clsd ` J ) A. x e. X ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) )

Proof

Step Hyp Ref Expression
1 simp1r 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( c e. ( Clsd ` J ) /\ x e. X ) /\ -. x e. c ) -> J e. Reg )
2 simp2l 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( c e. ( Clsd ` J ) /\ x e. X ) /\ -. x e. c ) -> c e. ( Clsd ` J ) )
3 simp2r 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( c e. ( Clsd ` J ) /\ x e. X ) /\ -. x e. c ) -> x e. X )
4 simp1l 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( c e. ( Clsd ` J ) /\ x e. X ) /\ -. x e. c ) -> J e. ( TopOn ` X ) )
5 toponuni 
 |-  ( J e. ( TopOn ` X ) -> X = U. J )
6 4 5 syl 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( c e. ( Clsd ` J ) /\ x e. X ) /\ -. x e. c ) -> X = U. J )
7 3 6 eleqtrd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( c e. ( Clsd ` J ) /\ x e. X ) /\ -. x e. c ) -> x e. U. J )
8 simp3 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( c e. ( Clsd ` J ) /\ x e. X ) /\ -. x e. c ) -> -. x e. c )
9 eqid 
 |-  U. J = U. J
10 9 regsep2 
 |-  ( ( J e. Reg /\ ( c e. ( Clsd ` J ) /\ x e. U. J /\ -. x e. c ) ) -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) )
11 1 2 7 8 10 syl13anc 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( c e. ( Clsd ` J ) /\ x e. X ) /\ -. x e. c ) -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) )
12 11 3expia 
 |-  ( ( ( J e. ( TopOn ` X ) /\ J e. Reg ) /\ ( c e. ( Clsd ` J ) /\ x e. X ) ) -> ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) )
13 12 ralrimivva 
 |-  ( ( J e. ( TopOn ` X ) /\ J e. Reg ) -> A. c e. ( Clsd ` J ) A. x e. X ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) )
14 topontop 
 |-  ( J e. ( TopOn ` X ) -> J e. Top )
15 14 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ A. c e. ( Clsd ` J ) A. x e. X ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> J e. Top )
16 5 adantr 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. J ) -> X = U. J )
17 16 difeq1d 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. J ) -> ( X \ y ) = ( U. J \ y ) )
18 9 opncld 
 |-  ( ( J e. Top /\ y e. J ) -> ( U. J \ y ) e. ( Clsd ` J ) )
19 14 18 sylan 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. J ) -> ( U. J \ y ) e. ( Clsd ` J ) )
20 17 19 eqeltrd 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. J ) -> ( X \ y ) e. ( Clsd ` J ) )
21 eleq2 
 |-  ( c = ( X \ y ) -> ( x e. c <-> x e. ( X \ y ) ) )
22 21 notbid 
 |-  ( c = ( X \ y ) -> ( -. x e. c <-> -. x e. ( X \ y ) ) )
23 eldif 
 |-  ( x e. ( X \ y ) <-> ( x e. X /\ -. x e. y ) )
24 23 baibr 
 |-  ( x e. X -> ( -. x e. y <-> x e. ( X \ y ) ) )
25 24 con1bid 
 |-  ( x e. X -> ( -. x e. ( X \ y ) <-> x e. y ) )
26 22 25 sylan9bb 
 |-  ( ( c = ( X \ y ) /\ x e. X ) -> ( -. x e. c <-> x e. y ) )
27 simpl 
 |-  ( ( c = ( X \ y ) /\ x e. X ) -> c = ( X \ y ) )
28 27 sseq1d 
 |-  ( ( c = ( X \ y ) /\ x e. X ) -> ( c C_ o <-> ( X \ y ) C_ o ) )
29 28 3anbi1d 
 |-  ( ( c = ( X \ y ) /\ x e. X ) -> ( ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) <-> ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) )
30 29 2rexbidv 
 |-  ( ( c = ( X \ y ) /\ x e. X ) -> ( E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) <-> E. o e. J E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) )
31 26 30 imbi12d 
 |-  ( ( c = ( X \ y ) /\ x e. X ) -> ( ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) <-> ( x e. y -> E. o e. J E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) )
32 31 ralbidva 
 |-  ( c = ( X \ y ) -> ( A. x e. X ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) <-> A. x e. X ( x e. y -> E. o e. J E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) )
33 32 rspcv 
 |-  ( ( X \ y ) e. ( Clsd ` J ) -> ( A. c e. ( Clsd ` J ) A. x e. X ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) -> A. x e. X ( x e. y -> E. o e. J E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) )
34 20 33 syl 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. J ) -> ( A. c e. ( Clsd ` J ) A. x e. X ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) -> A. x e. X ( x e. y -> E. o e. J E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) )
35 ralcom3 
 |-  ( A. x e. X ( x e. y -> E. o e. J E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) <-> A. x e. y ( x e. X -> E. o e. J E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) )
36 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. J ) -> y C_ X )
37 36 sselda 
 |-  ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) -> x e. X )
38 simprr2 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> x e. p )
39 5 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> X = U. J )
40 39 difeq1d 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> ( X \ o ) = ( U. J \ o ) )
41 14 ad3antrrr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> J e. Top )
42 simprll 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> o e. J )
43 9 opncld 
 |-  ( ( J e. Top /\ o e. J ) -> ( U. J \ o ) e. ( Clsd ` J ) )
44 41 42 43 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> ( U. J \ o ) e. ( Clsd ` J ) )
45 40 44 eqeltrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> ( X \ o ) e. ( Clsd ` J ) )
46 incom 
 |-  ( p i^i o ) = ( o i^i p )
47 simprr3 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> ( o i^i p ) = (/) )
48 46 47 syl5eq 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> ( p i^i o ) = (/) )
49 simplll 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> J e. ( TopOn ` X ) )
50 simprlr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> p e. J )
51 toponss 
 |-  ( ( J e. ( TopOn ` X ) /\ p e. J ) -> p C_ X )
52 49 50 51 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> p C_ X )
53 reldisj 
 |-  ( p C_ X -> ( ( p i^i o ) = (/) <-> p C_ ( X \ o ) ) )
54 52 53 syl 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> ( ( p i^i o ) = (/) <-> p C_ ( X \ o ) ) )
55 48 54 mpbid 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> p C_ ( X \ o ) )
56 9 clsss2 
 |-  ( ( ( X \ o ) e. ( Clsd ` J ) /\ p C_ ( X \ o ) ) -> ( ( cls ` J ) ` p ) C_ ( X \ o ) )
57 45 55 56 syl2anc 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> ( ( cls ` J ) ` p ) C_ ( X \ o ) )
58 simprr1 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> ( X \ y ) C_ o )
59 difcom 
 |-  ( ( X \ y ) C_ o <-> ( X \ o ) C_ y )
60 58 59 sylib 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> ( X \ o ) C_ y )
61 57 60 sstrd 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> ( ( cls ` J ) ` p ) C_ y )
62 38 61 jca 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( ( o e. J /\ p e. J ) /\ ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) )
63 62 expr 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ ( o e. J /\ p e. J ) ) -> ( ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) -> ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) ) )
64 63 anassrs 
 |-  ( ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ o e. J ) /\ p e. J ) -> ( ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) -> ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) ) )
65 64 reximdva 
 |-  ( ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) /\ o e. J ) -> ( E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) -> E. p e. J ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) ) )
66 65 rexlimdva 
 |-  ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) -> ( E. o e. J E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) -> E. p e. J ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) ) )
67 37 66 embantd 
 |-  ( ( ( J e. ( TopOn ` X ) /\ y e. J ) /\ x e. y ) -> ( ( x e. X -> E. o e. J E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) -> E. p e. J ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) ) )
68 67 ralimdva 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. J ) -> ( A. x e. y ( x e. X -> E. o e. J E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) -> A. x e. y E. p e. J ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) ) )
69 35 68 syl5bi 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. J ) -> ( A. x e. X ( x e. y -> E. o e. J E. p e. J ( ( X \ y ) C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) -> A. x e. y E. p e. J ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) ) )
70 34 69 syld 
 |-  ( ( J e. ( TopOn ` X ) /\ y e. J ) -> ( A. c e. ( Clsd ` J ) A. x e. X ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) -> A. x e. y E. p e. J ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) ) )
71 70 ralrimdva 
 |-  ( J e. ( TopOn ` X ) -> ( A. c e. ( Clsd ` J ) A. x e. X ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) -> A. y e. J A. x e. y E. p e. J ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) ) )
72 71 imp 
 |-  ( ( J e. ( TopOn ` X ) /\ A. c e. ( Clsd ` J ) A. x e. X ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> A. y e. J A. x e. y E. p e. J ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) )
73 isreg 
 |-  ( J e. Reg <-> ( J e. Top /\ A. y e. J A. x e. y E. p e. J ( x e. p /\ ( ( cls ` J ) ` p ) C_ y ) ) )
74 15 72 73 sylanbrc 
 |-  ( ( J e. ( TopOn ` X ) /\ A. c e. ( Clsd ` J ) A. x e. X ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) -> J e. Reg )
75 13 74 impbida 
 |-  ( J e. ( TopOn ` X ) -> ( J e. Reg <-> A. c e. ( Clsd ` J ) A. x e. X ( -. x e. c -> E. o e. J E. p e. J ( c C_ o /\ x e. p /\ ( o i^i p ) = (/) ) ) ) )