Metamath Proof Explorer

Theorem indishmph

Description: Equinumerous sets equipped with their indiscrete topologies are homeomorphic (which means in that particular case that a segment is homeomorphic to a circle contrary to what Wikipedia claims). (Contributed by FL, 17-Aug-2008) (Proof shortened by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion indishmph ( 𝐴 ≈ 𝐵 → { ∅ , 𝐴 } ≃ { ∅ , 𝐵 } )

Proof

Step Hyp Ref Expression
1 bren ⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
2 f1of ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 ⟶ 𝐵 )
3 f1odm ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → dom 𝑓 = 𝐴 )
4 vex ⊢ 𝑓 ∈ V
5 4 dmex ⊢ dom 𝑓 ∈ V
6 3 5 eqeltrrdi ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝐴 ∈ V )
7 f1ofo ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –onto→ 𝐵 )
8 fornex ⊢ ( 𝐴 ∈ V → ( 𝑓 : 𝐴 –onto→ 𝐵 → 𝐵 ∈ V ) )
9 6 7 8 sylc ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝐵 ∈ V )
10 9 6 elmapd ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) ↔ 𝑓 : 𝐴 ⟶ 𝐵 ) )
11 2 10 mpbird ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 ∈ ( 𝐵 ↑m 𝐴 ) )
12 indistopon ⊢ ( 𝐴 ∈ V → { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) )
13 6 12 syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) )
14 cnindis ⊢ ( ( { ∅ , 𝐴 } ∈ ( TopOn ‘ 𝐴 ) ∧ 𝐵 ∈ V ) → ( { ∅ , 𝐴 } Cn { ∅ , 𝐵 } ) = ( 𝐵 ↑m 𝐴 ) )
15 13 9 14 syl2anc ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( { ∅ , 𝐴 } Cn { ∅ , 𝐵 } ) = ( 𝐵 ↑m 𝐴 ) )
16 11 15 eleqtrrd ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 ∈ ( { ∅ , 𝐴 } Cn { ∅ , 𝐵 } ) )
17 f1ocnv ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 )
18 f1of ⊢ ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐵 ⟶ 𝐴 )
19 17 18 syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝑓 : 𝐵 ⟶ 𝐴 )
20 6 9 elmapd ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) ↔ ◡ 𝑓 : 𝐵 ⟶ 𝐴 ) )
21 19 20 mpbird ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝑓 ∈ ( 𝐴 ↑m 𝐵 ) )
22 indistopon ⊢ ( 𝐵 ∈ V → { ∅ , 𝐵 } ∈ ( TopOn ‘ 𝐵 ) )
23 9 22 syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → { ∅ , 𝐵 } ∈ ( TopOn ‘ 𝐵 ) )
24 cnindis ⊢ ( ( { ∅ , 𝐵 } ∈ ( TopOn ‘ 𝐵 ) ∧ 𝐴 ∈ V ) → ( { ∅ , 𝐵 } Cn { ∅ , 𝐴 } ) = ( 𝐴 ↑m 𝐵 ) )
25 23 6 24 syl2anc ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( { ∅ , 𝐵 } Cn { ∅ , 𝐴 } ) = ( 𝐴 ↑m 𝐵 ) )
26 21 25 eleqtrrd ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝑓 ∈ ( { ∅ , 𝐵 } Cn { ∅ , 𝐴 } ) )
27 ishmeo ⊢ ( 𝑓 ∈ ( { ∅ , 𝐴 } Homeo { ∅ , 𝐵 } ) ↔ ( 𝑓 ∈ ( { ∅ , 𝐴 } Cn { ∅ , 𝐵 } ) ∧ ◡ 𝑓 ∈ ( { ∅ , 𝐵 } Cn { ∅ , 𝐴 } ) ) )
28 16 26 27 sylanbrc ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 ∈ ( { ∅ , 𝐴 } Homeo { ∅ , 𝐵 } ) )
29 hmphi ⊢ ( 𝑓 ∈ ( { ∅ , 𝐴 } Homeo { ∅ , 𝐵 } ) → { ∅ , 𝐴 } ≃ { ∅ , 𝐵 } )
30 28 29 syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → { ∅ , 𝐴 } ≃ { ∅ , 𝐵 } )
31 30 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → { ∅ , 𝐴 } ≃ { ∅ , 𝐵 } )
32 1 31 sylbi ⊢ ( 𝐴 ≈ 𝐵 → { ∅ , 𝐴 } ≃ { ∅ , 𝐵 } )