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

Metamath Proof Explorer

Theorem ensn1

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002) Avoid ax-un . (Revised by BTernaryTau, 23-Sep-2024)

Ref Expression
Hypothesis ensn1.1 ⊢ 𝐴 ∈ V
Assertion ensn1 { 𝐴 } ≈ 1o

Proof

Step Hyp Ref Expression
1 ensn1.1 ⊢ 𝐴 ∈ V
2 snex ⊢ { ⟨ 𝐴 , ∅ ⟩ } ∈ V
3 f1oeq1 ⊢ ( 𝑓 = { ⟨ 𝐴 , ∅ ⟩ } → ( 𝑓 : { 𝐴 } –1-1-onto→ { ∅ } ↔ { ⟨ 𝐴 , ∅ ⟩ } : { 𝐴 } –1-1-onto→ { ∅ } ) )
4 0ex ⊢ ∅ ∈ V
5 1 4 f1osn ⊢ { ⟨ 𝐴 , ∅ ⟩ } : { 𝐴 } –1-1-onto→ { ∅ }
6 2 3 5 ceqsexv2d ⊢ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { ∅ }
7 snex ⊢ { 𝐴 } ∈ V
8 snex ⊢ { ∅ } ∈ V
9 breng ⊢ ( ( { 𝐴 } ∈ V ∧ { ∅ } ∈ V ) → ( { 𝐴 } ≈ { ∅ } ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { ∅ } ) )
10 7 8 9 mp2an ⊢ ( { 𝐴 } ≈ { ∅ } ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { ∅ } )
11 6 10 mpbir ⊢ { 𝐴 } ≈ { ∅ }
12 df1o2 ⊢ 1o = { ∅ }
13 11 12 breqtrri ⊢ { 𝐴 } ≈ 1o