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

Metamath Proof Explorer

Theorem en0

Description: The empty set is equinumerous only to itself. Exercise 1 of TakeutiZaring p. 88. (Contributed by NM, 27-May-1998) Avoid ax-pow , ax-un . (Revised by BTernaryTau, 23-Sep-2024)

Ref Expression
Assertion en0 ⊢ A ≈ ∅ ↔ A = ∅

Proof

Step Hyp Ref Expression
1 encv ⊢ A ≈ ∅ → A ∈ V ∧ ∅ ∈ V
2 breng ⊢ A ∈ V ∧ ∅ ∈ V → A ≈ ∅ ↔ ∃ f f : A ⟶ 1-1 onto ∅
3 1 2 syl ⊢ A ≈ ∅ → A ≈ ∅ ↔ ∃ f f : A ⟶ 1-1 onto ∅
4 3 ibi ⊢ A ≈ ∅ → ∃ f f : A ⟶ 1-1 onto ∅
5 f1ocnv ⊢ f : A ⟶ 1-1 onto ∅ → f -1 : ∅ ⟶ 1-1 onto A
6 f1o00 ⊢ f -1 : ∅ ⟶ 1-1 onto A ↔ f -1 = ∅ ∧ A = ∅
7 6 simprbi ⊢ f -1 : ∅ ⟶ 1-1 onto A → A = ∅
8 5 7 syl ⊢ f : A ⟶ 1-1 onto ∅ → A = ∅
9 8 exlimiv ⊢ ∃ f f : A ⟶ 1-1 onto ∅ → A = ∅
10 4 9 syl ⊢ A ≈ ∅ → A = ∅
11 0ex ⊢ ∅ ∈ V
12 f1oeq1 ⊢ f = ∅ → f : ∅ ⟶ 1-1 onto ∅ ↔ ∅ : ∅ ⟶ 1-1 onto ∅
13 f1o0 ⊢ ∅ : ∅ ⟶ 1-1 onto ∅
14 11 12 13 ceqsexv2d ⊢ ∃ f f : ∅ ⟶ 1-1 onto ∅
15 breng ⊢ ∅ ∈ V ∧ ∅ ∈ V → ∅ ≈ ∅ ↔ ∃ f f : ∅ ⟶ 1-1 onto ∅
16 11 11 15 mp2an ⊢ ∅ ≈ ∅ ↔ ∃ f f : ∅ ⟶ 1-1 onto ∅
17 14 16 mpbir ⊢ ∅ ≈ ∅
18 breq1 ⊢ A = ∅ → A ≈ ∅ ↔ ∅ ≈ ∅
19 17 18 mpbiri ⊢ A = ∅ → A ≈ ∅
20 10 19 impbii ⊢ A ≈ ∅ ↔ A = ∅