Metamath Proof Explorer

Theorem isnrm2

Description: An alternate characterization of normality. This is the important property in the proof of Urysohn's lemma. (Contributed by Jeff Hankins, 1-Feb-2010) (Proof shortened by Mario Carneiro, 24-Aug-2015)

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

Proof

Step Hyp Ref Expression
1 nrmtop 
 |-  ( J e. Nrm -> J e. Top )
2 nrmsep2 
 |-  ( ( J e. Nrm /\ ( c e. ( Clsd ` J ) /\ d e. ( Clsd ` J ) /\ ( c i^i d ) = (/) ) ) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) )
3 2 3exp2 
 |-  ( J e. Nrm -> ( c e. ( Clsd ` J ) -> ( d e. ( Clsd ` J ) -> ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) ) ) )
4 3 impd 
 |-  ( J e. Nrm -> ( ( c e. ( Clsd ` J ) /\ d e. ( Clsd ` J ) ) -> ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) ) )
5 4 ralrimivv 
 |-  ( J e. Nrm -> A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) )
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. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) ) )
7 simpl 
 |-  ( ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) ) -> J e. Top )
8 eqid 
 |-  U. J = U. J
9 8 opncld 
 |-  ( ( J e. Top /\ x e. J ) -> ( U. J \ x ) e. ( Clsd ` J ) )
10 9 adantr 
 |-  ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) -> ( U. J \ x ) e. ( Clsd ` J ) )
11 ineq2 
 |-  ( d = ( U. J \ x ) -> ( c i^i d ) = ( c i^i ( U. J \ x ) ) )
12 11 eqeq1d 
 |-  ( d = ( U. J \ x ) -> ( ( c i^i d ) = (/) <-> ( c i^i ( U. J \ x ) ) = (/) ) )
13 ineq2 
 |-  ( d = ( U. J \ x ) -> ( ( ( cls ` J ) ` o ) i^i d ) = ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) )
14 13 eqeq1d 
 |-  ( d = ( U. J \ x ) -> ( ( ( ( cls ` J ) ` o ) i^i d ) = (/) <-> ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) = (/) ) )
15 14 anbi2d 
 |-  ( d = ( U. J \ x ) -> ( ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) <-> ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) = (/) ) ) )
16 15 rexbidv 
 |-  ( d = ( U. J \ x ) -> ( E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) <-> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) = (/) ) ) )
17 12 16 imbi12d 
 |-  ( d = ( U. J \ x ) -> ( ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) <-> ( ( c i^i ( U. J \ x ) ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) = (/) ) ) ) )
18 17 rspcv 
 |-  ( ( U. J \ x ) e. ( Clsd ` J ) -> ( A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) -> ( ( c i^i ( U. J \ x ) ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) = (/) ) ) ) )
19 10 18 syl 
 |-  ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) -> ( A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) -> ( ( c i^i ( U. J \ x ) ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) = (/) ) ) ) )
20 inssdif0 
 |-  ( ( c i^i U. J ) C_ x <-> ( c i^i ( U. J \ x ) ) = (/) )
21 8 cldss 
 |-  ( c e. ( Clsd ` J ) -> c C_ U. J )
22 21 adantl 
 |-  ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) -> c C_ U. J )
23 dfss2 
 |-  ( c C_ U. J <-> ( c i^i U. J ) = c )
24 22 23 sylib 
 |-  ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) -> ( c i^i U. J ) = c )
25 24 sseq1d 
 |-  ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) -> ( ( c i^i U. J ) C_ x <-> c C_ x ) )
26 20 25 bitr3id 
 |-  ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) -> ( ( c i^i ( U. J \ x ) ) = (/) <-> c C_ x ) )
27 inssdif0 
 |-  ( ( ( ( cls ` J ) ` o ) i^i U. J ) C_ x <-> ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) = (/) )
28 simpll 
 |-  ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) -> J e. Top )
29 elssuni 
 |-  ( o e. J -> o C_ U. J )
30 8 clsss3 
 |-  ( ( J e. Top /\ o C_ U. J ) -> ( ( cls ` J ) ` o ) C_ U. J )
31 28 29 30 syl2an 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) /\ o e. J ) -> ( ( cls ` J ) ` o ) C_ U. J )
32 dfss2 
 |-  ( ( ( cls ` J ) ` o ) C_ U. J <-> ( ( ( cls ` J ) ` o ) i^i U. J ) = ( ( cls ` J ) ` o ) )
33 31 32 sylib 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) /\ o e. J ) -> ( ( ( cls ` J ) ` o ) i^i U. J ) = ( ( cls ` J ) ` o ) )
34 33 sseq1d 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) /\ o e. J ) -> ( ( ( ( cls ` J ) ` o ) i^i U. J ) C_ x <-> ( ( cls ` J ) ` o ) C_ x ) )
35 27 34 bitr3id 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) /\ o e. J ) -> ( ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) = (/) <-> ( ( cls ` J ) ` o ) C_ x ) )
36 35 anbi2d 
 |-  ( ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) /\ o e. J ) -> ( ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) = (/) ) <-> ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) )
37 36 rexbidva 
 |-  ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) -> ( E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) = (/) ) <-> E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) )
38 26 37 imbi12d 
 |-  ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) -> ( ( ( c i^i ( U. J \ x ) ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i ( U. J \ x ) ) = (/) ) ) <-> ( c C_ x -> E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) ) )
39 19 38 sylibd 
 |-  ( ( ( J e. Top /\ x e. J ) /\ c e. ( Clsd ` J ) ) -> ( A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) -> ( c C_ x -> E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) ) )
40 39 ralimdva 
 |-  ( ( J e. Top /\ x e. J ) -> ( A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) -> A. c e. ( Clsd ` J ) ( c C_ x -> E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) ) )
41 elin 
 |-  ( c e. ( ( Clsd ` J ) i^i ~P x ) <-> ( c e. ( Clsd ` J ) /\ c e. ~P x ) )
42 velpw 
 |-  ( c e. ~P x <-> c C_ x )
43 42 anbi2i 
 |-  ( ( c e. ( Clsd ` J ) /\ c e. ~P x ) <-> ( c e. ( Clsd ` J ) /\ c C_ x ) )
44 41 43 bitri 
 |-  ( c e. ( ( Clsd ` J ) i^i ~P x ) <-> ( c e. ( Clsd ` J ) /\ c C_ x ) )
45 44 imbi1i 
 |-  ( ( c e. ( ( Clsd ` J ) i^i ~P x ) -> E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) <-> ( ( c e. ( Clsd ` J ) /\ c C_ x ) -> E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) )
46 impexp 
 |-  ( ( ( c e. ( Clsd ` J ) /\ c C_ x ) -> E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) <-> ( c e. ( Clsd ` J ) -> ( c C_ x -> E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) ) )
47 45 46 bitri 
 |-  ( ( c e. ( ( Clsd ` J ) i^i ~P x ) -> E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) <-> ( c e. ( Clsd ` J ) -> ( c C_ x -> E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) ) )
48 47 ralbii2 
 |-  ( A. c e. ( ( Clsd ` J ) i^i ~P x ) E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) <-> A. c e. ( Clsd ` J ) ( c C_ x -> E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) )
49 40 48 imbitrrdi 
 |-  ( ( J e. Top /\ x e. J ) -> ( A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) -> A. c e. ( ( Clsd ` J ) i^i ~P x ) E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) )
50 49 ralrimdva 
 |-  ( J e. Top -> ( A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) -> A. x e. J A. c e. ( ( Clsd ` J ) i^i ~P x ) E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) )
51 50 imp 
 |-  ( ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) ) -> A. x e. J A. c e. ( ( Clsd ` J ) i^i ~P x ) E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) )
52 isnrm 
 |-  ( J e. Nrm <-> ( J e. Top /\ A. x e. J A. c e. ( ( Clsd ` J ) i^i ~P x ) E. o e. J ( c C_ o /\ ( ( cls ` J ) ` o ) C_ x ) ) )
53 7 51 52 sylanbrc 
 |-  ( ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) ) -> J e. Nrm )
54 6 53 impbii 
 |-  ( J e. Nrm <-> ( J e. Top /\ A. c e. ( Clsd ` J ) A. d e. ( Clsd ` J ) ( ( c i^i d ) = (/) -> E. o e. J ( c C_ o /\ ( ( ( cls ` J ) ` o ) i^i d ) = (/) ) ) ) )