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 ) )
4 3 adantl 
 |-  ( ( 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 )
8 4 adantr 
 |-  ( ( ( 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 )
15 14 ad2antlr 
 |-  ( ( ( 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 )
20 19 ad2antrl 
 |-  ( ( ( 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 )
31 30 adantr 
 |-  ( ( ( ( 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 )
33 18 adantr 
 |-  ( ( ( ( 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 )
40 39 ad2antrl 
 |-  ( ( ( ( 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 ) )
44 15 adantr 
 |-  ( ( ( ( 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 )
47 7 adantr 
 |-  ( ( ( ( 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 ) )