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 ( 𝐴 ≈ ∅ ↔ 𝐴 = ∅ )

Proof

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