Metamath Proof Explorer

Theorem isnrm3

Description: A topological space is normal iff any two disjoint closed sets are separated by open sets. (Contributed by Mario Carneiro, 24-Aug-2015)

Ref Expression
Assertion isnrm3 
|- ( J e. Nrm <-> ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) )

Proof

Step Hyp Ref Expression
1 nrmtop 
 |-  ( J e. Nrm -> J e. Top )
2 nrmsep 
 |-  ( ( J e. Nrm /\ ( c e. ( Clsd ` J ) /\ d e. ( Clsd ` J ) /\ ( c i^i d ) = (/) ) ) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) )
3 2 3exp2 
 |-  ( J e. Nrm -> ( c e. ( Clsd ` J ) -> ( d e. ( Clsd ` J ) -> ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) ) )
4 3 impd 
 |-  ( J e. Nrm -> ( ( c e. ( Clsd ` J ) /\ d e. ( Clsd ` J ) ) -> ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) )
5 4 ralrimivv 
 |-  ( J e. Nrm -> A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) )
6 1 5 jca 
 |-  ( J e. Nrm -> ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) )
7 simpl 
 |-  ( ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) -> J e. Top )
8 simpr1 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ y e. J ) /\ ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> c C_ x )
9 simpr2 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ y e. J ) /\ ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> d C_ y )
10 sslin 
 |-  ( d C_ y -> ( ( ( cls ` J ) ` x ) i^i d ) C_ ( ( ( cls ` J ) ` x ) i^i y ) )
11 9 10 syl 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ y e. J ) /\ ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> ( ( ( cls ` J ) ` x ) i^i d ) C_ ( ( ( cls ` J ) ` x ) i^i y ) )
12 eqid 
 |-  U. J = U. J
13 12 opncld 
 |-  ( ( J e. Top /\ y e. J ) -> ( U. J \ y ) e. ( Clsd ` J ) )
14 13 ad4ant13 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ y e. J ) /\ ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> ( U. J \ y ) e. ( Clsd ` J ) )
15 simpr3 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ y e. J ) /\ ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> ( x i^i y ) = (/) )
16 simpllr 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ y e. J ) /\ ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> x e. J )
17 elssuni 
 |-  ( x e. J -> x C_ U. J )
18 reldisj 
 |-  ( x C_ U. J -> ( ( x i^i y ) = (/) <-> x C_ ( U. J \ y ) ) )
19 16 17 18 3syl 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ y e. J ) /\ ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> ( ( x i^i y ) = (/) <-> x C_ ( U. J \ y ) ) )
20 15 19 mpbid 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ y e. J ) /\ ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> x C_ ( U. J \ y ) )
21 12 clsss2 
 |-  ( ( ( U. J \ y ) e. ( Clsd ` J ) /\ x C_ ( U. J \ y ) ) -> ( ( cls ` J ) ` x ) C_ ( U. J \ y ) )
22 ssdifin0 
 |-  ( ( ( cls ` J ) ` x ) C_ ( U. J \ y ) -> ( ( ( cls ` J ) ` x ) i^i y ) = (/) )
23 21 22 syl 
 |-  ( ( ( U. J \ y ) e. ( Clsd ` J ) /\ x C_ ( U. J \ y ) ) -> ( ( ( cls ` J ) ` x ) i^i y ) = (/) )
24 14 20 23 syl2anc 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ y e. J ) /\ ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> ( ( ( cls ` J ) ` x ) i^i y ) = (/) )
25 sseq0 
 |-  ( ( ( ( ( cls ` J ) ` x ) i^i d ) C_ ( ( ( cls ` J ) ` x ) i^i y ) /\ ( ( ( cls ` J ) ` x ) i^i y ) = (/) ) -> ( ( ( cls ` J ) ` x ) i^i d ) = (/) )
26 11 24 25 syl2anc 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ y e. J ) /\ ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> ( ( ( cls ` J ) ` x ) i^i d ) = (/) )
27 8 26 jca 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ y e. J ) /\ ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> ( c C_ x /\ ( ( ( cls ` J ) ` x ) i^i d ) = (/) ) )
28 27 rexlimdva2 
 |-  ( ( J e. Top /\ x e. J ) -> ( E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) -> ( c C_ x /\ ( ( ( cls ` J ) ` x ) i^i d ) = (/) ) ) )
29 28 reximdva 
 |-  ( J e. Top -> ( E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) -> E. x e. J ( c C_ x /\ ( ( ( cls ` J ) ` x ) i^i d ) = (/) ) ) )
30 29 imim2d 
 |-  ( J e. Top -> ( ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> ( ( c i^i d ) = (/) -> E. x e. J ( c C_ x /\ ( ( ( cls ` J ) ` x ) i^i d ) = (/) ) ) ) )
31 30 ralimdv 
 |-  ( J e. Top -> ( A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J ( c C_ x /\ ( ( ( cls ` J ) ` x ) i^i d ) = (/) ) ) ) )
32 31 ralimdv 
 |-  ( J e. Top -> ( A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) -> A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J ( c C_ x /\ ( ( ( cls ` J ) ` x ) i^i d ) = (/) ) ) ) )
33 32 imp 
 |-  ( ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) -> A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J ( c C_ x /\ ( ( ( cls ` J ) ` x ) i^i d ) = (/) ) ) )
34 isnrm2 
 |-  ( J e. Nrm <-> ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J ( c C_ x /\ ( ( ( cls ` J ) ` x ) i^i d ) = (/) ) ) ) )
35 7 33 34 sylanbrc 
 |-  ( ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) -> J e. Nrm )
36 6 35 impbii 
 |-  ( J e. Nrm <-> ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. x e. J E. y e. J ( c C_ x /\ d C_ y /\ ( x i^i y ) = (/) ) ) ) )