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 ∈ J Cn K | f -1 ∈ 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 -1 ∈ k Cn j ↔ f -1 ∈ K Cn J
5 1 4 rabeqbidv ⊢ j = J ∧ k = K → f ∈ j Cn k | f -1 ∈ k Cn j = f ∈ J Cn K | f -1 ∈ K Cn J
6 df-hmeo ⊢ Homeo = j ∈ Top , k ∈ Top ⟼ f ∈ j Cn k | f -1 ∈ k Cn j
7 ovex ⊢ J Cn K ∈ V
8 7 rabex ⊢ f ∈ J Cn K | f -1 ∈ K Cn J ∈ V
9 5 6 8 ovmpoa ⊢ J ∈ Top ∧ K ∈ Top → J Homeo K = f ∈ J Cn K | f -1 ∈ K Cn J
10 6 mpondm0 ⊢ ¬ J ∈ Top ∧ K ∈ Top → J Homeo K = ∅
11 cntop1 ⊢ f ∈ J Cn K → J ∈ Top
12 cntop2 ⊢ f ∈ J Cn K → K ∈ Top
13 11 12 jca ⊢ f ∈ J Cn K → J ∈ Top ∧ K ∈ Top
14 13 a1d ⊢ f ∈ J Cn K → f -1 ∈ K Cn J → J ∈ Top ∧ K ∈ Top
15 14 con3rr3 ⊢ ¬ J ∈ Top ∧ K ∈ Top → f ∈ J Cn K → ¬ f -1 ∈ K Cn J
16 15 ralrimiv ⊢ ¬ J ∈ Top ∧ K ∈ Top → ∀ f ∈ J Cn K ¬ f -1 ∈ K Cn J
17 rabeq0 ⊢ f ∈ J Cn K | f -1 ∈ K Cn J = ∅ ↔ ∀ f ∈ J Cn K ¬ f -1 ∈ K Cn J
18 16 17 sylibr ⊢ ¬ J ∈ Top ∧ K ∈ Top → f ∈ J Cn K | f -1 ∈ K Cn J = ∅
19 10 18 eqtr4d ⊢ ¬ J ∈ Top ∧ K ∈ Top → J Homeo K = f ∈ J Cn K | f -1 ∈ K Cn J
20 9 19 pm2.61i ⊢ J Homeo K = f ∈ J Cn K | f -1 ∈ K Cn J