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 A1𝑜xA=x

Proof

Step Hyp Ref Expression
1 df1o2 1𝑜=
2 1 breq2i A1𝑜A
3 encv AAVV
4 breng AVVAff:A1-1 onto
5 3 4 syl AAff:A1-1 onto
6 5 ibi Aff:A1-1 onto
7 2 6 sylbi A1𝑜ff:A1-1 onto
8 f1ocnv f:A1-1 ontof-1:1-1 ontoA
9 f1ofo f-1:1-1 ontoAf-1:ontoA
10 forn f-1:ontoAranf-1=A
11 9 10 syl f-1:1-1 ontoAranf-1=A
12 f1of f-1:1-1 ontoAf-1:A
13 0ex V
14 13 fsn2 f-1:Af-1Af-1=f-1
15 14 simprbi f-1:Af-1=f-1
16 12 15 syl f-1:1-1 ontoAf-1=f-1
17 16 rneqd f-1:1-1 ontoAranf-1=ranf-1
18 13 rnsnop ranf-1=f-1
19 17 18 eqtrdi f-1:1-1 ontoAranf-1=f-1
20 11 19 eqtr3d f-1:1-1 ontoAA=f-1
21 fvex f-1V
22 sneq x=f-1x=f-1
23 22 eqeq2d x=f-1A=xA=f-1
24 21 23 spcev A=f-1xA=x
25 8 20 24 3syl f:A1-1 ontoxA=x
26 25 exlimiv ff:A1-1 ontoxA=x
27 7 26 syl A1𝑜xA=x
28 vex xV
29 28 ensn1 x1𝑜
30 breq1 A=xA1𝑜x1𝑜
31 29 30 mpbiri A=xA1𝑜
32 31 exlimiv xA=xA1𝑜
33 27 32 impbii A1𝑜xA=x