Theorem ensn1

Description: A singleton is equinumerous to ordinal one. (Contributed by NM, 4-Nov-2002)

	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		bren	⊢ ( { 𝐴 } ≈ { ∅ } ↔ ∃ 𝑓 𝑓 : { 𝐴 } –1-1-onto→ { ∅ } )
8	6 7	mpbir	⊢ { 𝐴 } ≈ { ∅ }
9		df1o2	⊢ 1o = { ∅ }
10	8 9	breqtrri	⊢ { 𝐴 } ≈ 1o