This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( 𝐽 Homeo 𝐾 ) = { 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∣ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) }

Proof

Step Hyp Ref Expression
1 oveq12 ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) → ( 𝑗 Cn 𝑘 ) = ( 𝐽 Cn 𝐾 ) )
2 oveq12 ⊢ ( ( 𝑘 = 𝐾 ∧ 𝑗 = 𝐽 ) → ( 𝑘 Cn 𝑗 ) = ( 𝐾 Cn 𝐽 ) )
3 2 ancoms ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) → ( 𝑘 Cn 𝑗 ) = ( 𝐾 Cn 𝐽 ) )
4 3 eleq2d ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) → ( ◡ 𝑓 ∈ ( 𝑘 Cn 𝑗 ) ↔ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) ) )
5 1 4 rabeqbidv ⊢ ( ( 𝑗 = 𝐽 ∧ 𝑘 = 𝐾 ) → { 𝑓 ∈ ( 𝑗 Cn 𝑘 ) ∣ ◡ 𝑓 ∈ ( 𝑘 Cn 𝑗 ) } = { 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∣ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) } )
6 df-hmeo ⊢ Homeo = ( 𝑗 ∈ Top , 𝑘 ∈ Top ↦ { 𝑓 ∈ ( 𝑗 Cn 𝑘 ) ∣ ◡ 𝑓 ∈ ( 𝑘 Cn 𝑗 ) } )
7 ovex ⊢ ( 𝐽 Cn 𝐾 ) ∈ V
8 7 rabex ⊢ { 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∣ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) } ∈ V
9 5 6 8 ovmpoa ⊢ ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 Homeo 𝐾 ) = { 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∣ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) } )
10 6 mpondm0 ⊢ ( ¬ ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 Homeo 𝐾 ) = ∅ )
11 cntop1 ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝐽 ∈ Top )
12 cntop2 ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → 𝐾 ∈ Top )
13 11 12 jca ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) )
14 13 a1d ⊢ ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → ( ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ) )
15 14 con3rr3 ⊢ ( ¬ ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝑓 ∈ ( 𝐽 Cn 𝐾 ) → ¬ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) ) )
16 15 ralrimiv ⊢ ( ¬ ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ∀ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ¬ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) )
17 rabeq0 ⊢ ( { 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∣ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) } = ∅ ↔ ∀ 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ¬ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) )
18 16 17 sylibr ⊢ ( ¬ ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → { 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∣ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) } = ∅ )
19 10 18 eqtr4d ⊢ ( ¬ ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 Homeo 𝐾 ) = { 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∣ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) } )
20 9 19 pm2.61i ⊢ ( 𝐽 Homeo 𝐾 ) = { 𝑓 ∈ ( 𝐽 Cn 𝐾 ) ∣ ◡ 𝑓 ∈ ( 𝐾 Cn 𝐽 ) }