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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df1o2 | |
|
2 | 1 | breq2i | |
3 | encv | |
|
4 | breng | |
|
5 | 3 4 | syl | |
6 | 5 | ibi | |
7 | 2 6 | sylbi | |
8 | f1ocnv | |
|
9 | f1ofo | |
|
10 | forn | |
|
11 | 9 10 | syl | |
12 | f1of | |
|
13 | 0ex | |
|
14 | 13 | fsn2 | |
15 | 14 | simprbi | |
16 | 12 15 | syl | |
17 | 16 | rneqd | |
18 | 13 | rnsnop | |
19 | 17 18 | eqtrdi | |
20 | 11 19 | eqtr3d | |
21 | fvex | |
|
22 | sneq | |
|
23 | 22 | eqeq2d | |
24 | 21 23 | spcev | |
25 | 8 20 24 | 3syl | |
26 | 25 | exlimiv | |
27 | 7 26 | syl | |
28 | vex | |
|
29 | 28 | ensn1 | |
30 | breq1 | |
|
31 | 29 30 | mpbiri | |
32 | 31 | exlimiv | |
33 | 27 32 | impbii | |