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

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 f1o00 ⊢ ( 𝑓 : ∅ –1-1-onto→ 𝐴 ↔ ( 𝑓 = ∅ ∧ 𝐴 = ∅ ) )
6 5 simprbi ⊢ ( 𝑓 : ∅ –1-1-onto→ 𝐴 → 𝐴 = ∅ )
7 6 exlimiv ⊢ ( ∃ 𝑓 𝑓 : ∅ –1-1-onto→ 𝐴 → 𝐴 = ∅ )
8 4 7 syl ⊢ ( ∅ ≈ 𝐴 → 𝐴 = ∅ )
9 0ex ⊢ ∅ ∈ V
10 f1oeq1 ⊢ ( 𝑓 = ∅ → ( 𝑓 : ∅ –1-1-onto→ ∅ ↔ ∅ : ∅ –1-1-onto→ ∅ ) )
11 f1o0 ⊢ ∅ : ∅ –1-1-onto→ ∅
12 9 10 11 ceqsexv2d ⊢ ∃ 𝑓 𝑓 : ∅ –1-1-onto→ ∅
13 breng ⊢ ( ( ∅ ∈ V ∧ ∅ ∈ V ) → ( ∅ ≈ ∅ ↔ ∃ 𝑓 𝑓 : ∅ –1-1-onto→ ∅ ) )
14 9 9 13 mp2an ⊢ ( ∅ ≈ ∅ ↔ ∃ 𝑓 𝑓 : ∅ –1-1-onto→ ∅ )
15 12 14 mpbir ⊢ ∅ ≈ ∅
16 breq2 ⊢ ( 𝐴 = ∅ → ( ∅ ≈ 𝐴 ↔ ∅ ≈ ∅ ) )
17 15 16 mpbiri ⊢ ( 𝐴 = ∅ → ∅ ≈ 𝐴 )
18 8 17 impbii ⊢ ( ∅ ≈ 𝐴 ↔ 𝐴 = ∅ )