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