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 syl6bb
 |-  ( ( 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 )