HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version

Theorem wefrc 3850
Description: A non-empty (possibly proper) subclass of a class well-ordered by has a minimal element. Special case of Proposition 6.26 of [TakeutiZaring] p. 31.
Assertion
Ref Expression
wefrc
Distinct variable group:   ,
Allowed substitution hint:   ()

Proof of Theorem wefrc
StepHypRef Expression
1 wess 3843 . . 3
2 n0 3034 . . . 4
3 ineq2 2939 . . . . . . . . . . 11
43eqeq1d 2038 . . . . . . . . . 10
54rcla4ev 2526 . . . . . . . . 9
65ex 419 . . . . . . . 8
76adantl 445 . . . . . . 7
8 inss1 2963 . . . . . . . . . . 11
9 wefr 3846 . . . . . . . . . . . . 13
10 vex 2443 . . . . . . . . . . . . . . 15
1110inex2 3642 . . . . . . . . . . . . . 14
1211epfrc 3841 . . . . . . . . . . . . 13
139, 12syl3an1 1175 . . . . . . . . . . . 12
14133exp 1111 . . . . . . . . . . 11
158, 14mpi 16 . . . . . . . . . 10
16 elin 2933 . . . . . . . . . . . . 13
1716anbi1i 672 . . . . . . . . . . . 12
18 anass 625 . . . . . . . . . . . 12
1917, 18bitri 238 . . . . . . . . . . 11
2019rexbii2 2266 . . . . . . . . . 10
2115, 20syl6ib 215 . . . . . . . . 9
2221adantr 444 . . . . . . . 8
23 elin 2933 . . . . . . . . . . . . . . . . 17
24 df-3an 901 . . . . . . . . . . . . . . . . . . . . . . 23
25 3anrot 904 . . . . . . . . . . . . . . . . . . . . . . 23
2624, 25bitr3i 240 . . . . . . . . . . . . . . . . . . . . . 22
27 wetrep 3849 . . . . . . . . . . . . . . . . . . . . . . 23
2827exp3a 421 . . . . . . . . . . . . . . . . . . . . . 22
2926, 28sylan2b 454 . . . . . . . . . . . . . . . . . . . . 21
3029exp44 590 . . . . . . . . . . . . . . . . . . . 20
3130imp 414 . . . . . . . . . . . . . . . . . . 19
3231com34 77 . . . . . . . . . . . . . . . . . 18
3332imp3a 416 . . . . . . . . . . . . . . . . 17
3423, 33syl5bi 206 . . . . . . . . . . . . . . . 16
3534imp4a 566 . . . . . . . . . . . . . . 15
3635com23 72 . . . . . . . . . . . . . 14
3736ralrimdv 2319 . . . . . . . . . . . . 13
38 dfss3 2765 . . . . . . . . . . . . 13
3937, 38syl6ibr 216 . . . . . . . . . . . 12
40 dfss 2762 . . . . . . . . . . . . . . . 16
41 in32 2955 . . . . . . . . . . . . . . . . 17
4241eqeq2i 2040 . . . . . . . . . . . . . . . 16
4340, 42bitri 238 . . . . . . . . . . . . . . 15
4443biimpi 184 . . . . . . . . . . . . . 14
4544eqeq1d 2038 . . . . . . . . . . . . 13
4645biimprd 212 . . . . . . . . . . . 12
4739, 46syl6 29 . . . . . . . . . . 11
4847exp3a 421 . . . . . . . . . 10
4948imp4a 566 . . . . . . . . 9
5049reximdvai 2340 . . . . . . . 8
5122, 50syld 40 . . . . . . 7
527, 51pm2.61dne 2221 . . . . . 6
5352ex 419 . . . . 5
5453exlimdv 1747 . . . 4
552, 54syl5bi 206 . . 3
561, 55syl6com 31 . 2
57563imp 1106 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   w3a 899  wex 1447   wceq 1526   wcel 1528   wne 2147  wral 2239  wrex 2240   cin 2749   wss 2750  c0 3025   cep 3781   wfr 3824   wwe 3825
This theorem is referenced by:  tz7.5 3876  onnseq 5694  finminlem 20536
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1443  ax-6 1444  ax-7 1445  ax-gen 1446  ax-8 1530  ax-10 1531  ax-11 1532  ax-12 1533  ax-14 1535  ax-17 1542  ax-9 1557  ax-4 1563  ax-16 1741  ax-ext 2012  ax-sep 3626  ax-nul 3635  ax-pr 3695
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1448  df-sb 1703  df-eu 1930  df-mo 1931  df-clab 2018  df-cleq 2023  df-clel 2026  df-ne 2149  df-ral 2243  df-rex 2244  df-rab 2246  df-v 2442  df-dif 2753  df-un 2755  df-in 2757  df-ss 2761  df-nul 3026  df-if 3135  df-sn 3214  df-pr 3215  df-op 3217  df-br 3532  df-opab 3585  df-eprel 3783  df-po 3792  df-so 3806  df-fr 3826  df-we 3842
Copyright terms: Public domain