# 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 ) )`
` |-  ( ( 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 )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 )`
` |-  ( ( ( ( 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 ) )`