Metamath Proof Explorer

Theorem hmeoimaf1o

Description: The function mapping open sets to their images under a homeomorphism is a bijection of topologies. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Hypothesis hmeoimaf1o.1 
|- G = ( x e. J |-> ( F " x ) )
Assertion hmeoimaf1o 
|- ( F e. ( J Homeo K ) -> G : J -1-1-onto-> K )

Proof

Step Hyp Ref Expression
1 hmeoimaf1o.1 
 |-  G = ( x e. J |-> ( F " x ) )
2 hmeoima 
 |-  ( ( F e. ( J Homeo K ) /\ x e. J ) -> ( F " x ) e. K )
3 hmeocn 
 |-  ( F e. ( J Homeo K ) -> F e. ( J Cn K ) )
4 cnima 
 |-  ( ( F e. ( J Cn K ) /\ y e. K ) -> ( `' F " y ) e. J )
5 3 4 sylan 
 |-  ( ( F e. ( J Homeo K ) /\ y e. K ) -> ( `' F " y ) e. J )
6 eqid 
 |-  U. J = U. J
7 eqid 
 |-  U. K = U. K
8 6 7 hmeof1o 
 |-  ( F e. ( J Homeo K ) -> F : U. J -1-1-onto-> U. K )
9 8 adantr 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> F : U. J -1-1-onto-> U. K )
10 f1of1 
 |-  ( F : U. J -1-1-onto-> U. K -> F : U. J -1-1-> U. K )
11 9 10 syl 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> F : U. J -1-1-> U. K )
12 elssuni 
 |-  ( x e. J -> x C_ U. J )
13 12 ad2antrl 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> x C_ U. J )
14 cnvimass 
 |-  ( `' F " y ) C_ dom F
15 f1dm 
 |-  ( F : U. J -1-1-> U. K -> dom F = U. J )
16 11 15 syl 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> dom F = U. J )
17 14 16 sseqtrid 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> ( `' F " y ) C_ U. J )
18 f1imaeq 
 |-  ( ( F : U. J -1-1-> U. K /\ ( x C_ U. J /\ ( `' F " y ) C_ U. J ) ) -> ( ( F " x ) = ( F " ( `' F " y ) ) <-> x = ( `' F " y ) ) )
19 11 13 17 18 syl12anc 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> ( ( F " x ) = ( F " ( `' F " y ) ) <-> x = ( `' F " y ) ) )
20 f1ofo 
 |-  ( F : U. J -1-1-onto-> U. K -> F : U. J -onto-> U. K )
21 9 20 syl 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> F : U. J -onto-> U. K )
22 elssuni 
 |-  ( y e. K -> y C_ U. K )
23 22 ad2antll 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> y C_ U. K )
24 foimacnv 
 |-  ( ( F : U. J -onto-> U. K /\ y C_ U. K ) -> ( F " ( `' F " y ) ) = y )
25 21 23 24 syl2anc 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> ( F " ( `' F " y ) ) = y )
26 25 eqeq2d 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> ( ( F " x ) = ( F " ( `' F " y ) ) <-> ( F " x ) = y ) )
27 eqcom 
 |-  ( ( F " x ) = y <-> y = ( F " x ) )
28 26 27 bitrdi 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> ( ( F " x ) = ( F " ( `' F " y ) ) <-> y = ( F " x ) ) )
29 19 28 bitr3d 
 |-  ( ( F e. ( J Homeo K ) /\ ( x e. J /\ y e. K ) ) -> ( x = ( `' F " y ) <-> y = ( F " x ) ) )
30 1 2 5 29 f1o2d 
 |-  ( F e. ( J Homeo K ) -> G : J -1-1-onto-> K )