# Metamath Proof Explorer

## Theorem reghmph

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

Ref Expression
Assertion reghmph
`|- ( J ~= K -> ( J e. Reg -> K e. Reg ) )`

### 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. Reg /\ 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. Reg /\ f e. ( J Homeo K ) ) -> K e. Top )`
7 simpll
` |-  ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) -> J e. Reg )`
` |-  ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) -> f e. ( J Cn K ) )`
9 simprl
` |-  ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. 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. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) -> ( `' f " x ) e. J )`
12 eqid
` |-  U. J = U. J`
13 eqid
` |-  U. K = U. K`
14 12 13 hmeof1o
` |-  ( f e. ( J Homeo K ) -> f : U. J -1-1-onto-> U. K )`
` |-  ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) -> f : U. J -1-1-onto-> U. K )`
16 f1ocnv
` |-  ( f : U. J -1-1-onto-> U. K -> `' f : U. K -1-1-onto-> U. J )`
17 f1ofn
` |-  ( `' f : U. K -1-1-onto-> U. J -> `' f Fn U. K )`
18 15 16 17 3syl
` |-  ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) -> `' f Fn U. K )`
19 elssuni
` |-  ( x e. K -> x C_ U. K )`
` |-  ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) -> x C_ U. K )`
21 simprr
` |-  ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) -> y e. x )`
22 fnfvima
` |-  ( ( `' f Fn U. K /\ x C_ U. K /\ y e. x ) -> ( `' f ` y ) e. ( `' f " x ) )`
23 18 20 21 22 syl3anc
` |-  ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) -> ( `' f ` y ) e. ( `' f " x ) )`
24 regsep
` |-  ( ( J e. Reg /\ ( `' f " x ) e. J /\ ( `' f ` y ) e. ( `' f " x ) ) -> E. w e. J ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) )`
25 7 11 23 24 syl3anc
` |-  ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) -> E. w e. J ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) )`
26 simpllr
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> f e. ( J Homeo K ) )`
27 simprl
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> w e. J )`
28 hmeoima
` |-  ( ( f e. ( J Homeo K ) /\ w e. J ) -> ( f " w ) e. K )`
29 26 27 28 syl2anc
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( f " w ) e. K )`
30 20 21 sseldd
` |-  ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) -> y e. U. K )`
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> y e. U. K )`
32 simprrl
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( `' f ` y ) e. w )`
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> `' f Fn U. K )`
34 elpreima
` |-  ( `' f Fn U. K -> ( y e. ( `' `' f " w ) <-> ( y e. U. K /\ ( `' f ` y ) e. w ) ) )`
35 33 34 syl
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( y e. ( `' `' f " w ) <-> ( y e. U. K /\ ( `' f ` y ) e. w ) ) )`
36 31 32 35 mpbir2and
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> y e. ( `' `' f " w ) )`
37 imacnvcnv
` |-  ( `' `' f " w ) = ( f " w )`
38 36 37 eleqtrdi
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> y e. ( f " w ) )`
39 elssuni
` |-  ( w e. J -> w C_ U. J )`
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> w C_ U. J )`
41 12 hmeocls
` |-  ( ( f e. ( J Homeo K ) /\ w C_ U. J ) -> ( ( cls ` K ) ` ( f " w ) ) = ( f " ( ( cls ` J ) ` w ) ) )`
42 26 40 41 syl2anc
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( ( cls ` K ) ` ( f " w ) ) = ( f " ( ( cls ` J ) ` w ) ) )`
43 simprrr
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( ( cls ` J ) ` w ) C_ ( `' f " x ) )`
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> f : U. J -1-1-onto-> U. K )`
45 f1ofun
` |-  ( f : U. J -1-1-onto-> U. K -> Fun f )`
46 44 45 syl
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> Fun f )`
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> J e. Reg )`
48 regtop
` |-  ( J e. Reg -> J e. Top )`
49 47 48 syl
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> J e. Top )`
50 12 clsss3
` |-  ( ( J e. Top /\ w C_ U. J ) -> ( ( cls ` J ) ` w ) C_ U. J )`
51 49 40 50 syl2anc
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. 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 44 52 syl
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> dom f = U. J )`
54 51 53 sseqtrrd
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. 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 46 54 55 syl2anc
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( ( f " ( ( cls ` J ) ` w ) ) C_ x <-> ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) )`
57 43 56 mpbird
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( f " ( ( cls ` J ) ` w ) ) C_ x )`
58 42 57 eqsstrd
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> ( ( cls ` K ) ` ( f " w ) ) C_ x )`
59 eleq2
` |-  ( z = ( f " w ) -> ( y e. z <-> y e. ( 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 e. z /\ ( ( cls ` K ) ` z ) C_ x ) <-> ( y e. ( f " w ) /\ ( ( cls ` K ) ` ( f " w ) ) C_ x ) ) )`
63 62 rspcev
` |-  ( ( ( f " w ) e. K /\ ( y e. ( f " w ) /\ ( ( cls ` K ) ` ( f " w ) ) C_ x ) ) -> E. z e. K ( y e. z /\ ( ( cls ` K ) ` z ) C_ x ) )`
64 29 38 58 63 syl12anc
` |-  ( ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) /\ ( w e. J /\ ( ( `' f ` y ) e. w /\ ( ( cls ` J ) ` w ) C_ ( `' f " x ) ) ) ) -> E. z e. K ( y e. z /\ ( ( cls ` K ) ` z ) C_ x ) )`
65 25 64 rexlimddv
` |-  ( ( ( J e. Reg /\ f e. ( J Homeo K ) ) /\ ( x e. K /\ y e. x ) ) -> E. z e. K ( y e. z /\ ( ( cls ` K ) ` z ) C_ x ) )`
66 65 ralrimivva
` |-  ( ( J e. Reg /\ f e. ( J Homeo K ) ) -> A. x e. K A. y e. x E. z e. K ( y e. z /\ ( ( cls ` K ) ` z ) C_ x ) )`
67 isreg
` |-  ( K e. Reg <-> ( K e. Top /\ A. x e. K A. y e. x E. z e. K ( y e. z /\ ( ( cls ` K ) ` z ) C_ x ) ) )`
68 6 66 67 sylanbrc
` |-  ( ( J e. Reg /\ f e. ( J Homeo K ) ) -> K e. Reg )`
69 68 expcom
` |-  ( f e. ( J Homeo K ) -> ( J e. Reg -> K e. Reg ) )`
70 69 exlimiv
` |-  ( E. f f e. ( J Homeo K ) -> ( J e. Reg -> K e. Reg ) )`
71 2 70 sylbi
` |-  ( ( J Homeo K ) =/= (/) -> ( J e. Reg -> K e. Reg ) )`
72 1 71 sylbi
` |-  ( J ~= K -> ( J e. Reg -> K e. Reg ) )`