This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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