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

Theorem wefrc 3926
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 3919 . . 3
2 n0 3094 . . . 4
3 ineq2 2999 . . . . . . . . . . 11
43eqeq1d 2098 . . . . . . . . . 10
54rcla4ev 2586 . . . . . . . . 9
65ex 419 . . . . . . . 8
76adantl 445 . . . . . . 7
8 inss1 3023 . . . . . . . . . . 11
9 wefr 3922 . . . . . . . . . . . . 13
10 vex 2503 . . . . . . . . . . . . . . 15
1110inex2 3703 . . . . . . . . . . . . . 14
1211epfrc 3918 . . . . . . . . . . . . 13
139, 12syl3an1 1178 . . . . . . . . . . . 12
14133exp 1114 . . . . . . . . . . 11
158, 14mpi 16 . . . . . . . . . 10
16 elin 2993 . . . . . . . . . . . . 13
1716anbi1i 672 . . . . . . . . . . . 12
18 anass 625 . . . . . . . . . . . 12
1917, 18bitri 238 . . . . . . . . . . 11
2019rexbii2 2326 . . . . . . . . . 10
2115, 20syl6ib 215 . . . . . . . . 9
2221adantr 444 . . . . . . . 8
23 elin 2993 . . . . . . . . . . . . . . . . 17
24 df-3an 901 . . . . . . . . . . . . . . . . . . . . . . 23
25 3anrot 904 . . . . . . . . . . . . . . . . . . . . . . 23
2624, 25bitr3i 240 . . . . . . . . . . . . . . . . . . . . . 22
27 wetrep 3925 . . . . . . . . . . . . . . . . . . . . . . 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 2379 . . . . . . . . . . . . 13
38 dfss3 2825 . . . . . . . . . . . . 13
3937, 38syl6ibr 216 . . . . . . . . . . . 12
40 dfss 2822 . . . . . . . . . . . . . . . 16
41 in32 3015 . . . . . . . . . . . . . . . . 17
4241eqeq2i 2100 . . . . . . . . . . . . . . . 16
4340, 42bitri 238 . . . . . . . . . . . . . . 15
4443biimpi 184 . . . . . . . . . . . . . 14
4544eqeq1d 2098 . . . . . . . . . . . . 13
4645biimprd 212 . . . . . . . . . . . 12
4739, 46syl6 29 . . . . . . . . . . 11
4847exp3a 421 . . . . . . . . . 10
4948imp4a 566 . . . . . . . . 9
5049reximdvai 2400 . . . . . . . 8
5122, 50syld 40 . . . . . . 7
527, 51pm2.61dne 2281 . . . . . 6
5352ex 419 . . . . 5
5453exlimdv 1797 . . . 4
552, 54syl5bi 206 . . 3
561, 55syl6com 31 . 2
57563imp 1109 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 357   w3a 899  wex 1450   wceq 1531   wcel 1533   wne 2207  wral 2299  wrex 2300   cin 2809   wss 2810  c0 3085   cep 3842   wfr 3888   wwe 3890
This theorem is referenced by:  tz7.5  3952  onnseq  5787  finminlem  20830
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1446  ax-6 1447  ax-7 1448  ax-gen 1449  ax-8 1535  ax-11 1536  ax-12 1537  ax-14 1539  ax-17 1542  ax-9 1563  ax-10 1591  ax-4 1605  ax-16 1790  ax-ext 2072  ax-sep 3687  ax-nul 3696  ax-pr 3756
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1451  df-sb 1751  df-eu 1984  df-mo 1985  df-clab 2078  df-cleq 2083  df-clel 2086  df-ne 2209  df-ral 2303  df-rex 2304  df-rab 2306  df-v 2502  df-dif 2813  df-un 2815  df-in 2817  df-ss 2821  df-nul 3086  df-if 3195  df-sn 3274  df-pr 3275  df-op 3277  df-br 3592  df-opab 3645  df-eprel 3844  df-po 3853  df-so 3854  df-fr 3891  df-we 3893
Copyright terms: Public domain