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 𝐽 ) }