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 ⊢ A ≈ B → ∅ A ≃ ∅ B

Proof

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