Metamath Proof Explorer

Theorem hmeofval

Description: The set of all the homeomorphisms between two topologies. (Contributed by FL, 14-Feb-2007) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Assertion hmeofval 
|- ( J Homeo K ) = { f e. ( J Cn K ) | `' f e. ( K Cn J ) }

Proof

Step Hyp Ref Expression
1 oveq12 
 |-  ( ( j = J /\ k = K ) -> ( j Cn k ) = ( J Cn K ) )
2 oveq12 
 |-  ( ( k = K /\ j = J ) -> ( k Cn j ) = ( K Cn J ) )
3 2 ancoms 
 |-  ( ( j = J /\ k = K ) -> ( k Cn j ) = ( K Cn J ) )
4 3 eleq2d 
 |-  ( ( j = J /\ k = K ) -> ( `' f e. ( k Cn j ) <-> `' f e. ( K Cn J ) ) )
5 1 4 rabeqbidv 
 |-  ( ( j = J /\ k = K ) -> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } = { f e. ( J Cn K ) | `' f e. ( K Cn J ) } )
6 df-hmeo 
 |-  Homeo = ( j e. Top , k e. Top |-> { f e. ( j Cn k ) | `' f e. ( k Cn j ) } )
7 ovex 
 |-  ( J Cn K ) e. _V
8 7 rabex 
 |-  { f e. ( J Cn K ) | `' f e. ( K Cn J ) } e. _V
9 5 6 8 ovmpoa 
 |-  ( ( J e. Top /\ K e. Top ) -> ( J Homeo K ) = { f e. ( J Cn K ) | `' f e. ( K Cn J ) } )
10 6 mpondm0 
 |-  ( -. ( J e. Top /\ K e. Top ) -> ( J Homeo K ) = (/) )
11 cntop1 
 |-  ( f e. ( J Cn K ) -> J e. Top )
12 cntop2 
 |-  ( f e. ( J Cn K ) -> K e. Top )
13 11 12 jca 
 |-  ( f e. ( J Cn K ) -> ( J e. Top /\ K e. Top ) )
14 13 a1d 
 |-  ( f e. ( J Cn K ) -> ( `' f e. ( K Cn J ) -> ( J e. Top /\ K e. Top ) ) )
15 14 con3rr3 
 |-  ( -. ( J e. Top /\ K e. Top ) -> ( f e. ( J Cn K ) -> -. `' f e. ( K Cn J ) ) )
16 15 ralrimiv 
 |-  ( -. ( J e. Top /\ K e. Top ) -> A. f e. ( J Cn K ) -. `' f e. ( K Cn J ) )
17 rabeq0 
 |-  ( { f e. ( J Cn K ) | `' f e. ( K Cn J ) } = (/) <-> A. f e. ( J Cn K ) -. `' f e. ( K Cn J ) )
18 16 17 sylibr 
 |-  ( -. ( J e. Top /\ K e. Top ) -> { f e. ( J Cn K ) | `' f e. ( K Cn J ) } = (/) )
19 10 18 eqtr4d 
 |-  ( -. ( J e. Top /\ K e. Top ) -> ( J Homeo K ) = { f e. ( J Cn K ) | `' f e. ( K Cn J ) } )
20 9 19 pm2.61i 
 |-  ( J Homeo K ) = { f e. ( J Cn K ) | `' f e. ( K Cn J ) }