Theorem hmphen2

Description: Homeomorphisms preserve the cardinality of the underlying sets. (Contributed by FL, 17-Aug-2008) (Revised by Mario Carneiro, 10-Sep-2015)

	Ref	Expression
Hypotheses	cmphaushmeo.1	⊢ 𝑋 = ∪ 𝐽
	cmphaushmeo.2	⊢ 𝑌 = ∪ 𝐾
Assertion	hmphen2	⊢ ( 𝐽 ≃ 𝐾 → 𝑋 ≈ 𝑌 )

Proof

Step	Hyp	Ref	Expression
1		cmphaushmeo.1	⊢ 𝑋 = ∪ 𝐽
2		cmphaushmeo.2	⊢ 𝑌 = ∪ 𝐾
3		hmph	⊢ ( 𝐽 ≃ 𝐾 ↔ ( 𝐽 Homeo 𝐾 ) ≠ ∅ )
4		n0	⊢ ( ( 𝐽 Homeo 𝐾 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) )
5	1 2	hmeof1o	⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝑓 : 𝑋 –1-1-onto→ 𝑌 )
6		f1oen3g	⊢ ( ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) ∧ 𝑓 : 𝑋 –1-1-onto→ 𝑌 ) → 𝑋 ≈ 𝑌 )
7	5 6	mpdan	⊢ ( 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝑋 ≈ 𝑌 )
8	7	exlimiv	⊢ ( ∃ 𝑓 𝑓 ∈ ( 𝐽 Homeo 𝐾 ) → 𝑋 ≈ 𝑌 )
9	4 8	sylbi	⊢ ( ( 𝐽 Homeo 𝐾 ) ≠ ∅ → 𝑋 ≈ 𝑌 )
10	3 9	sylbi	⊢ ( 𝐽 ≃ 𝐾 → 𝑋 ≈ 𝑌 )