Theorem en1

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004)

	Ref	Expression
Assertion	en1	⊢ ( 𝐴 ≈ 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		df1o2	⊢ 1o = { ∅ }
2	1	breq2i	⊢ ( 𝐴 ≈ 1o ↔ 𝐴 ≈ { ∅ } )
3		bren	⊢ ( 𝐴 ≈ { ∅ } ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ { ∅ } )
4	2 3	bitri	⊢ ( 𝐴 ≈ 1o ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ { ∅ } )
5		f1ocnv	⊢ ( 𝑓 : 𝐴 –1-1-onto→ { ∅ } → ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 )
6		f1ofo	⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ◡ 𝑓 : { ∅ } –onto→ 𝐴 )
7		forn	⊢ ( ◡ 𝑓 : { ∅ } –onto→ 𝐴 → ran ◡ 𝑓 = 𝐴 )
8	6 7	syl	⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ran ◡ 𝑓 = 𝐴 )
9		f1of	⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ◡ 𝑓 : { ∅ } ⟶ 𝐴 )
10		0ex	⊢ ∅ ∈ V
11	10	fsn2	⊢ ( ◡ 𝑓 : { ∅ } ⟶ 𝐴 ↔ ( ( ◡ 𝑓 ‘ ∅ ) ∈ 𝐴 ∧ ◡ 𝑓 = { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ } ) )
12	11	simprbi	⊢ ( ◡ 𝑓 : { ∅ } ⟶ 𝐴 → ◡ 𝑓 = { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ } )
13	9 12	syl	⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ◡ 𝑓 = { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ } )
14	13	rneqd	⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ran ◡ 𝑓 = ran { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ } )
15	10	rnsnop	⊢ ran { ⟨ ∅ , ( ◡ 𝑓 ‘ ∅ ) ⟩ } = { ( ◡ 𝑓 ‘ ∅ ) }
16	14 15	syl6eq	⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → ran ◡ 𝑓 = { ( ◡ 𝑓 ‘ ∅ ) } )
17	8 16	eqtr3d	⊢ ( ◡ 𝑓 : { ∅ } –1-1-onto→ 𝐴 → 𝐴 = { ( ◡ 𝑓 ‘ ∅ ) } )
18		fvex	⊢ ( ◡ 𝑓 ‘ ∅ ) ∈ V
19		sneq	⊢ ( 𝑥 = ( ◡ 𝑓 ‘ ∅ ) → { 𝑥 } = { ( ◡ 𝑓 ‘ ∅ ) } )
20	19	eqeq2d	⊢ ( 𝑥 = ( ◡ 𝑓 ‘ ∅ ) → ( 𝐴 = { 𝑥 } ↔ 𝐴 = { ( ◡ 𝑓 ‘ ∅ ) } ) )
21	18 20	spcev	⊢ ( 𝐴 = { ( ◡ 𝑓 ‘ ∅ ) } → ∃ 𝑥 𝐴 = { 𝑥 } )
22	5 17 21	3syl	⊢ ( 𝑓 : 𝐴 –1-1-onto→ { ∅ } → ∃ 𝑥 𝐴 = { 𝑥 } )
23	22	exlimiv	⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ { ∅ } → ∃ 𝑥 𝐴 = { 𝑥 } )
24	4 23	sylbi	⊢ ( 𝐴 ≈ 1o → ∃ 𝑥 𝐴 = { 𝑥 } )
25		vex	⊢ 𝑥 ∈ V
26	25	ensn1	⊢ { 𝑥 } ≈ 1o
27		breq1	⊢ ( 𝐴 = { 𝑥 } → ( 𝐴 ≈ 1o ↔ { 𝑥 } ≈ 1o ) )
28	26 27	mpbiri	⊢ ( 𝐴 = { 𝑥 } → 𝐴 ≈ 1o )
29	28	exlimiv	⊢ ( ∃ 𝑥 𝐴 = { 𝑥 } → 𝐴 ≈ 1o )
30	24 29	impbii	⊢ ( 𝐴 ≈ 1o ↔ ∃ 𝑥 𝐴 = { 𝑥 } )