Metamath Proof Explorer


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 ↔ ∃ 𝑥 𝐴 = { 𝑥 } )