Metamath Proof Explorer

Theorem regsep2

Description: In a regular space, a closed set is separated by open sets from a point not in it. (Contributed by Jeff Hankins, 1-Feb-2010) (Revised by Mario Carneiro, 25-Aug-2015)

Ref Expression
Hypothesis t1sep.1 
|- X = U. J
Assertion regsep2 
|- ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> E. x e. J E. y e. J ( C C_ x /\ A e. y /\ ( x i^i y ) = (/) ) )

Proof

Step Hyp Ref Expression
1 t1sep.1 
 |-  X = U. J
2 regtop 
 |-  ( J e. Reg -> J e. Top )
3 2 ad2antrr 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> J e. Top )
4 elssuni 
 |-  ( y e. J -> y C_ U. J )
5 4 1 sseqtrrdi 
 |-  ( y e. J -> y C_ X )
6 5 ad2antrl 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> y C_ X )
7 1 clscld 
 |-  ( ( J e. Top /\ y C_ X ) -> ( ( cls ` J ) ` y ) e. ( Clsd ` J ) )
8 3 6 7 syl2anc 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> ( ( cls ` J ) ` y ) e. ( Clsd ` J ) )
9 1 cldopn 
 |-  ( ( ( cls ` J ) ` y ) e. ( Clsd ` J ) -> ( X \ ( ( cls ` J ) ` y ) ) e. J )
10 8 9 syl 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> ( X \ ( ( cls ` J ) ` y ) ) e. J )
11 simprrr 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> ( ( cls ` J ) ` y ) C_ ( X \ C ) )
12 1 clsss3 
 |-  ( ( J e. Top /\ y C_ X ) -> ( ( cls ` J ) ` y ) C_ X )
13 3 6 12 syl2anc 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> ( ( cls ` J ) ` y ) C_ X )
14 simplr1 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> C e. ( Clsd ` J ) )
15 1 cldss 
 |-  ( C e. ( Clsd ` J ) -> C C_ X )
16 14 15 syl 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> C C_ X )
17 ssconb 
 |-  ( ( ( ( cls ` J ) ` y ) C_ X /\ C C_ X ) -> ( ( ( cls ` J ) ` y ) C_ ( X \ C ) <-> C C_ ( X \ ( ( cls ` J ) ` y ) ) ) )
18 13 16 17 syl2anc 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> ( ( ( cls ` J ) ` y ) C_ ( X \ C ) <-> C C_ ( X \ ( ( cls ` J ) ` y ) ) ) )
19 11 18 mpbid 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> C C_ ( X \ ( ( cls ` J ) ` y ) ) )
20 simprrl 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> A e. y )
21 1 sscls 
 |-  ( ( J e. Top /\ y C_ X ) -> y C_ ( ( cls ` J ) ` y ) )
22 3 6 21 syl2anc 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> y C_ ( ( cls ` J ) ` y ) )
23 sslin 
 |-  ( y C_ ( ( cls ` J ) ` y ) -> ( ( X \ ( ( cls ` J ) ` y ) ) i^i y ) C_ ( ( X \ ( ( cls ` J ) ` y ) ) i^i ( ( cls ` J ) ` y ) ) )
24 22 23 syl 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> ( ( X \ ( ( cls ` J ) ` y ) ) i^i y ) C_ ( ( X \ ( ( cls ` J ) ` y ) ) i^i ( ( cls ` J ) ` y ) ) )
25 incom 
 |-  ( ( X \ ( ( cls ` J ) ` y ) ) i^i ( ( cls ` J ) ` y ) ) = ( ( ( cls ` J ) ` y ) i^i ( X \ ( ( cls ` J ) ` y ) ) )
26 disjdif 
 |-  ( ( ( cls ` J ) ` y ) i^i ( X \ ( ( cls ` J ) ` y ) ) ) = (/)
27 25 26 eqtri 
 |-  ( ( X \ ( ( cls ` J ) ` y ) ) i^i ( ( cls ` J ) ` y ) ) = (/)
28 sseq0 
 |-  ( ( ( ( X \ ( ( cls ` J ) ` y ) ) i^i y ) C_ ( ( X \ ( ( cls ` J ) ` y ) ) i^i ( ( cls ` J ) ` y ) ) /\ ( ( X \ ( ( cls ` J ) ` y ) ) i^i ( ( cls ` J ) ` y ) ) = (/) ) -> ( ( X \ ( ( cls ` J ) ` y ) ) i^i y ) = (/) )
29 24 27 28 sylancl 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> ( ( X \ ( ( cls ` J ) ` y ) ) i^i y ) = (/) )
30 sseq2 
 |-  ( x = ( X \ ( ( cls ` J ) ` y ) ) -> ( C C_ x <-> C C_ ( X \ ( ( cls ` J ) ` y ) ) ) )
31 ineq1 
 |-  ( x = ( X \ ( ( cls ` J ) ` y ) ) -> ( x i^i y ) = ( ( X \ ( ( cls ` J ) ` y ) ) i^i y ) )
32 31 eqeq1d 
 |-  ( x = ( X \ ( ( cls ` J ) ` y ) ) -> ( ( x i^i y ) = (/) <-> ( ( X \ ( ( cls ` J ) ` y ) ) i^i y ) = (/) ) )
33 30 32 3anbi13d 
 |-  ( x = ( X \ ( ( cls ` J ) ` y ) ) -> ( ( C C_ x /\ A e. y /\ ( x i^i y ) = (/) ) <-> ( C C_ ( X \ ( ( cls ` J ) ` y ) ) /\ A e. y /\ ( ( X \ ( ( cls ` J ) ` y ) ) i^i y ) = (/) ) ) )
34 33 rspcev 
 |-  ( ( ( X \ ( ( cls ` J ) ` y ) ) e. J /\ ( C C_ ( X \ ( ( cls ` J ) ` y ) ) /\ A e. y /\ ( ( X \ ( ( cls ` J ) ` y ) ) i^i y ) = (/) ) ) -> E. x e. J ( C C_ x /\ A e. y /\ ( x i^i y ) = (/) ) )
35 10 19 20 29 34 syl13anc 
 |-  ( ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) /\ ( y e. J /\ ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) ) ) -> E. x e. J ( C C_ x /\ A e. y /\ ( x i^i y ) = (/) ) )
36 simpl 
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> J e. Reg )
37 simpr1 
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> C e. ( Clsd ` J ) )
38 1 cldopn 
 |-  ( C e. ( Clsd ` J ) -> ( X \ C ) e. J )
39 37 38 syl 
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> ( X \ C ) e. J )
40 simpr2 
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> A e. X )
41 simpr3 
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> -. A e. C )
42 40 41 eldifd 
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> A e. ( X \ C ) )
43 regsep 
 |-  ( ( J e. Reg /\ ( X \ C ) e. J /\ A e. ( X \ C ) ) -> E. y e. J ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) )
44 36 39 42 43 syl3anc 
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> E. y e. J ( A e. y /\ ( ( cls ` J ) ` y ) C_ ( X \ C ) ) )
45 35 44 reximddv 
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> E. y e. J E. x e. J ( C C_ x /\ A e. y /\ ( x i^i y ) = (/) ) )
46 rexcom 
 |-  ( E. y e. J E. x e. J ( C C_ x /\ A e. y /\ ( x i^i y ) = (/) ) <-> E. x e. J E. y e. J ( C C_ x /\ A e. y /\ ( x i^i y ) = (/) ) )
47 45 46 sylib 
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> E. x e. J E. y e. J ( C C_ x /\ A e. y /\ ( x i^i y ) = (/) ) )