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

Metamath Proof Explorer

Theorem en0r

Description: The empty set is equinumerous only to itself. (Contributed by BTernaryTau, 29-Nov-2024)

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

Proof

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