Description: Every nonempty class of numerable sets has a minimal element. (Contributed by BTernaryTau, 18-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | nummin | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cardf2 | |
|
2 | ffun | |
|
3 | 2 | funfnd | |
4 | 1 3 | ax-mp | |
5 | fnimaeq0 | |
|
6 | 4 5 | mpan | |
7 | 6 | necon3bid | |
8 | 7 | biimprd | |
9 | 8 | imdistani | |
10 | fimass | |
|
11 | 1 10 | ax-mp | |
12 | onssmin | |
|
13 | 11 12 | mpan | |
14 | ssel | |
|
15 | ssel | |
|
16 | 14 15 | anim12d | |
17 | 11 16 | ax-mp | |
18 | ontri1 | |
|
19 | 17 18 | syl | |
20 | epel | |
|
21 | 20 | notbii | |
22 | 19 21 | bitr4di | |
23 | 22 | rgen2 | |
24 | r19.29r | |
|
25 | 13 23 24 | sylancl | |
26 | r19.26 | |
|
27 | bicom1 | |
|
28 | 27 | biimparc | |
29 | 28 | ralimi | |
30 | 26 29 | sylbir | |
31 | 30 | reximi | |
32 | 25 31 | syl | |
33 | 32 | adantl | |
34 | breq2 | |
|
35 | 34 | notbid | |
36 | 35 | ralbidv | |
37 | 36 | rexima | |
38 | 4 37 | mpan | |
39 | 38 | adantr | |
40 | 33 39 | mpbid | |
41 | fvex | |
|
42 | 41 | dfpred3 | |
43 | 42 | eqeq1i | |
44 | rabeq0 | |
|
45 | 43 44 | bitri | |
46 | 45 | rexbii | |
47 | 40 46 | sylibr | |
48 | 9 47 | syl | |
49 | ssel2 | |
|
50 | cardpred | |
|
51 | 50 | eqeq1d | |
52 | predss | |
|
53 | sstr | |
|
54 | 52 53 | mpan | |
55 | fnimaeq0 | |
|
56 | 4 54 55 | sylancr | |
57 | 56 | adantr | |
58 | 51 57 | bitrd | |
59 | 49 58 | syldan | |
60 | 59 | rexbidva | |
61 | 60 | adantr | |
62 | 48 61 | mpbid | |