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 disjdifr
 |-  ( ( X \ ( ( cls ` J ) ` y ) ) i^i ( ( cls ` J ) ` y ) ) = (/)
26 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 ) = (/) )
27 24 25 26 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 ) = (/) )
28 sseq2
 |-  ( x = ( X \ ( ( cls ` J ) ` y ) ) -> ( C C_ x <-> C C_ ( X \ ( ( cls ` J ) ` y ) ) ) )
29 ineq1
 |-  ( x = ( X \ ( ( cls ` J ) ` y ) ) -> ( x i^i y ) = ( ( X \ ( ( cls ` J ) ` y ) ) i^i y ) )
30 29 eqeq1d
 |-  ( x = ( X \ ( ( cls ` J ) ` y ) ) -> ( ( x i^i y ) = (/) <-> ( ( X \ ( ( cls ` J ) ` y ) ) i^i y ) = (/) ) )
31 28 30 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 ) = (/) ) ) )
32 31 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 ) = (/) ) )
33 10 19 20 27 32 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 ) = (/) ) )
34 simpl
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> J e. Reg )
35 simpr1
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> C e. ( Clsd ` J ) )
36 1 cldopn
 |-  ( C e. ( Clsd ` J ) -> ( X \ C ) e. J )
37 35 36 syl
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> ( X \ C ) e. J )
38 simpr2
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> A e. X )
39 simpr3
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> -. A e. C )
40 38 39 eldifd
 |-  ( ( J e. Reg /\ ( C e. ( Clsd ` J ) /\ A e. X /\ -. A e. C ) ) -> A e. ( X \ C ) )
41 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 ) ) )
42 34 37 40 41 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 ) ) )
43 33 42 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 ) = (/) ) )
44 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 ) = (/) ) )
45 43 44 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 ) = (/) ) )