Metamath Proof Explorer


Theorem nummin

Description: Every nonempty class of numerable sets has a minimal element. (Contributed by BTernaryTau, 18-Jul-2024)

Ref Expression
Assertion nummin AdomcardAxAPredAx=

Proof

Step Hyp Ref Expression
1 cardf2 card:z|yOnyzOn
2 ffun card:z|yOnyzOnFuncard
3 2 funfnd card:z|yOnyzOncardFndomcard
4 1 3 ax-mp cardFndomcard
5 fnimaeq0 cardFndomcardAdomcardcardA=A=
6 4 5 mpan AdomcardcardA=A=
7 6 necon3bid AdomcardcardAA
8 7 biimprd AdomcardAcardA
9 8 imdistani AdomcardAAdomcardcardA
10 fimass card:z|yOnyzOncardAOn
11 1 10 ax-mp cardAOn
12 onssmin cardAOncardAzcardAycardAzy
13 11 12 mpan cardAzcardAycardAzy
14 ssel cardAOnzcardAzOn
15 ssel cardAOnycardAyOn
16 14 15 anim12d cardAOnzcardAycardAzOnyOn
17 11 16 ax-mp zcardAycardAzOnyOn
18 ontri1 zOnyOnzy¬yz
19 17 18 syl zcardAycardAzy¬yz
20 epel yEzyz
21 20 notbii ¬yEz¬yz
22 19 21 bitr4di zcardAycardAzy¬yEz
23 22 rgen2 zcardAycardAzy¬yEz
24 r19.29r zcardAycardAzyzcardAycardAzy¬yEzzcardAycardAzyycardAzy¬yEz
25 13 23 24 sylancl cardAzcardAycardAzyycardAzy¬yEz
26 r19.26 ycardAzyzy¬yEzycardAzyycardAzy¬yEz
27 bicom1 zy¬yEz¬yEzzy
28 27 biimparc zyzy¬yEz¬yEz
29 28 ralimi ycardAzyzy¬yEzycardA¬yEz
30 26 29 sylbir ycardAzyycardAzy¬yEzycardA¬yEz
31 30 reximi zcardAycardAzyycardAzy¬yEzzcardAycardA¬yEz
32 25 31 syl cardAzcardAycardA¬yEz
33 32 adantl AdomcardcardAzcardAycardA¬yEz
34 breq2 z=cardxyEzyEcardx
35 34 notbid z=cardx¬yEz¬yEcardx
36 35 ralbidv z=cardxycardA¬yEzycardA¬yEcardx
37 36 rexima cardFndomcardAdomcardzcardAycardA¬yEzxAycardA¬yEcardx
38 4 37 mpan AdomcardzcardAycardA¬yEzxAycardA¬yEcardx
39 38 adantr AdomcardcardAzcardAycardA¬yEzxAycardA¬yEcardx
40 33 39 mpbid AdomcardcardAxAycardA¬yEcardx
41 fvex cardxV
42 41 dfpred3 PredEcardAcardx=ycardA|yEcardx
43 42 eqeq1i PredEcardAcardx=ycardA|yEcardx=
44 rabeq0 ycardA|yEcardx=ycardA¬yEcardx
45 43 44 bitri PredEcardAcardx=ycardA¬yEcardx
46 45 rexbii xAPredEcardAcardx=xAycardA¬yEcardx
47 40 46 sylibr AdomcardcardAxAPredEcardAcardx=
48 9 47 syl AdomcardAxAPredEcardAcardx=
49 ssel2 AdomcardxAxdomcard
50 cardpred AdomcardxdomcardPredEcardAcardx=cardPredAx
51 50 eqeq1d AdomcardxdomcardPredEcardAcardx=cardPredAx=
52 predss PredAxA
53 sstr PredAxAAdomcardPredAxdomcard
54 52 53 mpan AdomcardPredAxdomcard
55 fnimaeq0 cardFndomcardPredAxdomcardcardPredAx=PredAx=
56 4 54 55 sylancr AdomcardcardPredAx=PredAx=
57 56 adantr AdomcardxdomcardcardPredAx=PredAx=
58 51 57 bitrd AdomcardxdomcardPredEcardAcardx=PredAx=
59 49 58 syldan AdomcardxAPredEcardAcardx=PredAx=
60 59 rexbidva AdomcardxAPredEcardAcardx=xAPredAx=
61 60 adantr AdomcardAxAPredEcardAcardx=xAPredAx=
62 48 61 mpbid AdomcardAxAPredAx=