Theorem en1

Description: A set is equinumerous to ordinal one iff it is a singleton. (Contributed by NM, 25-Jul-2004) Avoid ax-un . (Revised by BTernaryTau, 23-Sep-2024)

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

Proof

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