Theorem tz6.26 14558
 Description: All nonempty (possibly proper) subclasses of , which has a well-founded relation , have -minimal elements. Proposition 6.26 of [TakeutiZaring] p. 31.
Assertion
Ref Expression
tz6.26 Pred Pred
Distinct variable groups:   ,   ,   ,   ,   ,   ,

Proof of Theorem tz6.26
StepHypRef Expression
1 wess 3799 . . . 4
2 cbvsetlike 14534 . . . . 5 Pred Pred
3 ssralv 2899 . . . . . 6 Pred Pred
4 predpredss 14525 . . . . . . . 8 Pred Pred
5 ssexg 3624 . . . . . . . . 9 Pred Pred Pred Pred
65ex 398 . . . . . . . 8 Pred Pred Pred Pred
74, 6syl 13 . . . . . . 7 Pred Pred
87ralimdv 2422 . . . . . 6 Pred Pred
93, 8syld 33 . . . . 5 Pred Pred
102, 9syl5bi 249 . . . 4 Pred Pred
111, 10anim12d 533 . . 3 Pred Pred
12 n0 3091 . . . 4
13 predeq3 14524 . . . . . . . . . . 11 Pred Pred
1413eqeq1d 2149 . . . . . . . . . 10 Pred Pred
1514rcla4ev 2620 . . . . . . . . 9 Pred Pred
1615ex 398 . . . . . . . 8 Pred Pred
1716adantl 448 . . . . . . 7 Pred Pred Pred
18 predss 14526 . . . . . . . . . 10 Pred
19 wefr 3802 . . . . . . . . . . . . 13
20 predeq3 14524 . . . . . . . . . . . . . . 15 Pred Pred
2120eleq1d 2210 . . . . . . . . . . . . . 14 Pred Pred
2221rcla4cva 2619 . . . . . . . . . . . . 13 Pred Pred
2319, 22anim12i 536 . . . . . . . . . . . 12 Pred Pred
2423anassrs 632 . . . . . . . . . . 11 Pred Pred
25 sseq1 2865 . . . . . . . . . . . . . . . 16 Pred Pred
26 neeq1 2273 . . . . . . . . . . . . . . . 16 Pred Pred
2725, 26anbi12d 763 . . . . . . . . . . . . . . 15 Pred Pred Pred
28 predeq2 14523 . . . . . . . . . . . . . . . . 17 Pred Pred Pred Pred
2928eqeq1d 2149 . . . . . . . . . . . . . . . 16 Pred Pred Pred Pred
3029rexeqbi1dv 2518 . . . . . . . . . . . . . . 15 Pred Pred Pred Pred Pred
3127, 30imbi12d 761 . . . . . . . . . . . . . 14 Pred Pred Pred Pred Pred Pred Pred
3231imbi2d 747 . . . . . . . . . . . . 13 Pred Pred Pred Pred Pred Pred Pred
33 dffr4 14535 . . . . . . . . . . . . . 14 Pred
34 ax-4 1608 . . . . . . . . . . . . . 14 Pred Pred
3533, 34sylbi 225 . . . . . . . . . . . . 13 Pred
3632, 35vtoclg 2588 . . . . . . . . . . . 12 Pred Pred Pred Pred Pred Pred
3736impcom 394 . . . . . . . . . . 11 Pred Pred Pred Pred Pred Pred
3824, 37syl 13 . . . . . . . . . 10 Pred Pred Pred Pred Pred Pred
3918, 38mpani 686 . . . . . . . . 9 Pred Pred Pred Pred Pred
40 weso 3803 . . . . . . . . . . . . 13
4140anim1i 538 . . . . . . . . . . . 12
42 visset 2541 . . . . . . . . . . . . . 14
43 visset 2541 . . . . . . . . . . . . . . 15
4443elpred 14530 . . . . . . . . . . . . . 14 Pred
4542, 44ax-mp 7 . . . . . . . . . . . . 13 Pred
4645biimpi 224 . . . . . . . . . . . 12 Pred
47 sotr 3770 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
48473exp2 1335 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
4948com23 65 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
5049com34 75 . . . . . . . . . . . . . . . . . . . . . . . . . 26
51503imp 1311 . . . . . . . . . . . . . . . . . . . . . . . . 25
5251com23 65 . . . . . . . . . . . . . . . . . . . . . . . 24
5352exp3a 400 . . . . . . . . . . . . . . . . . . . . . . 23
5453com23 65 . . . . . . . . . . . . . . . . . . . . . 22
55543exp 1316 . . . . . . . . . . . . . . . . . . . . 21
5655com23 65 . . . . . . . . . . . . . . . . . . . 20
5756imp43 571 . . . . . . . . . . . . . . . . . . 19
58573imp 1311 . . . . . . . . . . . . . . . . . 18
59 elpredg 14531 . . . . . . . . . . . . . . . . . . . . 21 Pred
6059adantll 775 . . . . . . . . . . . . . . . . . . . 20 Pred
6160adantlr 777 . . . . . . . . . . . . . . . . . . 19 Pred
62613adant2 1139 . . . . . . . . . . . . . . . . . 18 Pred
6358, 62mpbird 318 . . . . . . . . . . . . . . . . 17 Pred
64633exp 1316 . . . . . . . . . . . . . . . 16 Pred
6564imdistand 772 . . . . . . . . . . . . . . 15 Pred
66 visset 2541 . . . . . . . . . . . . . . . . . 18
6766elpred 14530 . . . . . . . . . . . . . . . . 17 Pred
6843, 67ax-mp 7 . . . . . . . . . . . . . . . 16 Pred
69 ancom 414 . . . . . . . . . . . . . . . 16
7068, 69bitri 279 . . . . . . . . . . . . . . 15 Pred
7166elpred 14530 . . . . . . . . . . . . . . . . 17 Pred Pred Pred
7243, 71ax-mp 7 . . . . . . . . . . . . . . . 16 Pred Pred Pred
73 ancom 414 . . . . . . . . . . . . . . . 16 Pred Pred
7472, 73bitri 279 . . . . . . . . . . . . . . 15 Pred Pred Pred
7565, 70, 743imtr4g 332 . . . . . . . . . . . . . 14 Pred Pred Pred
7675ssrdv 2853 . . . . . . . . . . . . 13 Pred Pred Pred
77 sseq0 3110 . . . . . . . . . . . . . 14 Pred Pred Pred Pred Pred Pred
7877ex 398 . . . . . . . . . . . . 13 Pred Pred Pred Pred Pred Pred
7976, 78syl 13 . . . . . . . . . . . 12 Pred Pred Pred
8041, 46, 79syl2an 603 . . . . . . . . . . 11 Pred Pred Pred Pred
8180reximdva 2453 . . . . . . . . . 10 Pred Pred Pred Pred Pred
8281adantlr 777 . . . . . . . . 9 Pred Pred Pred Pred Pred Pred
8339, 82syld 33 . . . . . . . 8 Pred Pred Pred Pred
84 ssrexv 2900 . . . . . . . . 9 Pred Pred Pred Pred
8518, 84ax-mp 7 . . . . . . . 8 Pred Pred Pred
8683, 85syl6 42 . . . . . . 7 Pred Pred Pred
8717, 86pm2.61dne 2340 . . . . . 6 Pred Pred
8887ex 398 . . . . 5 Pred Pred
898819.23adv 1860 . . . 4 Pred Pred
9012, 89syl5bi 249 . . 3 Pred Pred
9111, 90syl6com 102 . 2 Pred Pred
9291imp32 397 1 Pred Pred
 Colors of variables: wff set class Syntax hints:   wi 3   wb 219   wa 337   w3a 1102  wal 1584   wceq 1586   wcel 1588  wex 1615   wne 2266  wral 2355  wrex 2356  cvv 2538   wss 2827  c0 3082   class class class wbr 3507   wor 3751   wfr 3780   wwe 3781  Predcpred 14520 This theorem is referenced by:  tz6.26i 14559  wfi 14560 This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687 This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-v 2540  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-br 3508  df-opab 3566  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-xp 4133  df-cnv 4135  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-pred 14521