Metamath Proof Explorer

Theorem nrmhmph

Description: Normality is a topological property. (Contributed by Mario Carneiro, 25-Aug-2015)

Ref Expression
Assertion nrmhmph 
|- ( J ~= K -> ( J e. Nrm -> K e. Nrm ) )

Proof

Step Hyp Ref Expression
1 hmph 
 |-  ( J ~= K <-> ( J Homeo K ) =/= (/) )
2 n0 
 |-  ( ( J Homeo K ) =/= (/) <-> E. f f e. ( J Homeo K ) )
3 hmeocn 
 |-  ( f e. ( J Homeo K ) -> f e. ( J Cn K ) )
4 3 adantl 
 |-  ( ( J e. Nrm /\ f e. ( J Homeo K ) ) -> f e. ( J Cn K ) )
5 cntop2 
 |-  ( f e. ( J Cn K ) -> K e. Top )
6 4 5 syl 
 |-  ( ( J e. Nrm /\ f e. ( J Homeo K ) ) -> K e. Top )
7 simpll 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> J e. Nrm )
8 4 adantr 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> f e. ( J Cn K ) )
9 simprl 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> x e. K )
10 cnima 
 |-  ( ( f e. ( J Cn K ) /\ x e. K ) -> ( `' f " x ) e. J )
11 8 9 10 syl2anc 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> ( `' f " x ) e. J )
12 simprr 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> y e. ( ( Clsd ` K ) i^i ~P x ) )
13 12 elin1d 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> y e. ( Clsd ` K ) )
14 cnclima 
 |-  ( ( f e. ( J Cn K ) /\ y e. ( Clsd ` K ) ) -> ( `' f " y ) e. ( Clsd ` J ) )
15 8 13 14 syl2anc 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> ( `' f " y ) e. ( Clsd ` J ) )
16 12 elin2d 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> y e. ~P x )
17 16 elpwid 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> y C_ x )
18 imass2 
 |-  ( y C_ x -> ( `' f " y ) C_ ( `' f " x ) )
19 17 18 syl 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> ( `' f " y ) C_ ( `' f " x ) )
20 nrmsep3 
 |-  ( ( J e. Nrm /\ ( ( `' f " x ) e. J /\ ( `' f " y ) e. ( Clsd ` J ) /\ ( `' f " y ) C_ ( `' f " x ) ) ) -> E. w e. J ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) )
21 7 11 15 19 20 syl13anc 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> E. w e. J ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) )
22 simpllr 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> f e. ( J Homeo K ) )
23 simprl 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> w e. J )
24 hmeoima 
 |-  ( ( f e. ( J Homeo K ) /\ w e. J ) -> ( f " w ) e. K )
25 22 23 24 syl2anc 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( f " w ) e. K )
26 simprrl 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( `' f " y ) C_ w )
27 eqid 
 |-  U. J = U. J
28 eqid 
 |-  U. K = U. K
29 27 28 hmeof1o 
 |-  ( f e. ( J Homeo K ) -> f : U. J -1-1-onto-> U. K )
30 22 29 syl 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> f : U. J -1-1-onto-> U. K )
31 f1ofun 
 |-  ( f : U. J -1-1-onto-> U. K -> Fun f )
32 30 31 syl 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> Fun f )
33 13 adantr 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> y e. ( Clsd ` K ) )
34 28 cldss 
 |-  ( y e. ( Clsd ` K ) -> y C_ U. K )
35 33 34 syl 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> y C_ U. K )
36 f1ofo 
 |-  ( f : U. J -1-1-onto-> U. K -> f : U. J -onto-> U. K )
37 forn 
 |-  ( f : U. J -onto-> U. K -> ran f = U. K )
38 30 36 37 3syl 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ran f = U. K )
39 35 38 sseqtrrd 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> y C_ ran f )
40 funimass1 
 |-  ( ( Fun f /\ y C_ ran f ) -> ( ( `' f " y ) C_ w -> y C_ ( f " w ) ) )
41 32 39 40 syl2anc 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( ( `' f " y ) C_ w -> y C_ ( f " w ) ) )
42 26 41 mpd 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> y C_ ( f " w ) )
43 elssuni 
 |-  ( w e. J -> w C_ U. J )
44 43 ad2antrl 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> w C_ U. J )
45 27 hmeocls 
 |-  ( ( f e. ( J Homeo K ) /\ w C_ U. J ) -> ( ( cls ` K ) ` ( f " w ) ) = ( f " ( ( cls ` J ) ` w ) ) )
46 22 44 45 syl2anc 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( ( cls ` K ) ` ( f " w ) ) = ( f " ( ( cls ` J ) ` w ) ) )
47 simprrr 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( ( cls ` J ) ` w ) C_ ( `' f " x ) )
48 nrmtop 
 |-  ( J e. Nrm -> J e. Top )
49 48 ad3antrrr 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> J e. Top )
50 27 clsss3 
 |-  ( ( J e. Top /\ w C_ U. J ) -> ( ( cls ` J ) ` w ) C_ U. J )
51 49 44 50 syl2anc 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( ( cls ` J ) ` w ) C_ U. J )
52 f1odm 
 |-  ( f : U. J -1-1-onto-> U. K -> dom f = U. J )
53 30 52 syl 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> dom f = U. J )
54 51 53 sseqtrrd 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( ( cls ` J ) ` w ) C_ dom f )
55 funimass3 
 |-  ( ( Fun f /\ ( ( cls ` J ) ` w ) C_ dom f ) -> ( ( f " ( ( cls ` J ) ` w ) ) C_ x <-> ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) )
56 32 54 55 syl2anc 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( ( f " ( ( cls ` J ) ` w ) ) C_ x <-> ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) )
57 47 56 mpbird 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( f " ( ( cls ` J ) ` w ) ) C_ x )
58 46 57 eqsstrd 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( ( cls ` K ) ` ( f " w ) ) C_ x )
59 sseq2 
 |-  ( z = ( f " w ) -> ( y C_ z <-> y C_ ( f " w ) ) )
60 fveq2 
 |-  ( z = ( f " w ) -> ( ( cls ` K ) ` z ) = ( ( cls ` K ) ` ( f " w ) ) )
61 60 sseq1d 
 |-  ( z = ( f " w ) -> ( ( ( cls ` K ) ` z ) C_ x <-> ( ( cls ` K ) ` ( f " w ) ) C_ x ) )
62 59 61 anbi12d 
 |-  ( z = ( f " w ) -> ( ( y C_ z /\ ( ( cls ` K ) ` z ) C_ x ) <-> ( y C_ ( f " w ) /\ ( ( cls ` K ) ` ( f " w ) ) C_ x ) ) )
63 62 rspcev 
 |-  ( ( ( f " w ) e. K /\ ( y C_ ( f " w ) /\ ( ( cls ` K ) ` ( f " w ) ) C_ x ) ) -> E. z e. K ( y C_ z /\ ( ( cls ` K ) ` z ) C_ x ) )
64 25 42 58 63 syl12anc 
 |-  ( ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) /\ ( w e. J /\ ( ( `' f " y ) C_ w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> E. z e. K ( y C_ z /\ ( ( cls ` K ) ` z ) C_ x ) )
65 21 64 rexlimddv 
 |-  ( ( ( J e. Nrm /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. ( ( Clsd ` K ) i^i ~P x ) ) ) -> E. z e. K ( y C_ z /\ ( ( cls ` K ) ` z ) C_ x ) )
66 65 ralrimivva 
 |-  ( ( J e. Nrm /\ f e. ( J Homeo K ) ) -> A. x e. K A. y e. ( ( Clsd ` K ) i^i ~P x ) E. z e. K ( y C_ z /\ ( ( cls ` K ) ` z ) C_ x ) )
67 isnrm 
 |-  ( K e. Nrm <-> ( K e. Top /\ A. x e. K A. y e. ( ( Clsd ` K ) i^i ~P x ) E. z e. K ( y C_ z /\ ( ( cls ` K ) ` z ) C_ x ) ) )
68 6 66 67 sylanbrc 
 |-  ( ( J e. Nrm /\ f e. ( J Homeo K ) ) -> K e. Nrm )
69 68 expcom 
 |-  ( f e. ( J Homeo K ) -> ( J e. Nrm -> K e. Nrm ) )
70 69 exlimiv 
 |-  ( E. f f e. ( J Homeo K ) -> ( J e. Nrm -> K e. Nrm ) )
71 2 70 sylbi 
 |-  ( ( J Homeo K ) =/= (/) -> ( J e. Nrm -> K e. Nrm ) )
72 1 71 sylbi 
 |-  ( J ~= K -> ( J e. Nrm -> K e. Nrm ) )