Metamath Proof Explorer


Theorem en1OLD

Description: Obsolete version of en1 as of 23-Sep-2024. (Contributed by NM, 25-Jul-2004) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion en1OLD ( 𝐴 ≈ 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 eqtrdi ( 𝑓 : { ∅ } –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 ↔ ∃ 𝑥 𝐴 = { 𝑥 } )