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

Theorem wefrc 3674
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 3667 . . 3
2 n0 2907 . . . 4
3 ineq2 2814 . . . . . . . . . . 11
43eqeq1d 1925 . . . . . . . . . 10
54rcla4ev 2408 . . . . . . . . 9
65ex 418 . . . . . . . 8
76adantl 444 . . . . . . 7
8 inss1 2838 . . . . . . . . . . 11
9 wefr 3670 . . . . . . . . . . . . 13
10 vex 2325 . . . . . . . . . . . . . . 15
1110inex2 3470 . . . . . . . . . . . . . 14
1211epfrc 3665 . . . . . . . . . . . . 13
139, 12syl3an1 1174 . . . . . . . . . . . 12
14133exp 1110 . . . . . . . . . . 11
158, 14mpi 15 . . . . . . . . . 10
16 elin 2810 . . . . . . . . . . . . 13
1716anbi1i 671 . . . . . . . . . . . 12
18 anass 624 . . . . . . . . . . . 12
1917, 18bitri 237 . . . . . . . . . . 11
2019rexbii2 2152 . . . . . . . . . 10
2115, 20syl6ib 214 . . . . . . . . 9
2221adantr 443 . . . . . . . 8
23 elin 2810 . . . . . . . . . . . . . . . . 17
24 df-3an 900 . . . . . . . . . . . . . . . . . . . . . . 23
25 3anrot 903 . . . . . . . . . . . . . . . . . . . . . . 23
2624, 25bitr3i 239 . . . . . . . . . . . . . . . . . . . . . 22
27 wetrep 3673 . . . . . . . . . . . . . . . . . . . . . . 23
2827exp3a 420 . . . . . . . . . . . . . . . . . . . . . 22
2926, 28sylan2b 453 . . . . . . . . . . . . . . . . . . . . 21
3029exp44 589 . . . . . . . . . . . . . . . . . . . 20
3130imp 413 . . . . . . . . . . . . . . . . . . 19
3231com34 76 . . . . . . . . . . . . . . . . . 18
3332imp3a 415 . . . . . . . . . . . . . . . . 17
3423, 33syl5bi 205 . . . . . . . . . . . . . . . 16
3534imp4a 565 . . . . . . . . . . . . . . 15
3635com23 71 . . . . . . . . . . . . . 14
3736ralrimdv 2205 . . . . . . . . . . . . 13
38 dfss3 2647 . . . . . . . . . . . . 13
3937, 38syl6ibr 215 . . . . . . . . . . . 12
40 dfss 2642 . . . . . . . . . . . . . . . 16
41 in32 2830 . . . . . . . . . . . . . . . . 17
4241eqeq2i 1927 . . . . . . . . . . . . . . . 16
4340, 42bitri 237 . . . . . . . . . . . . . . 15
4443biimpi 183 . . . . . . . . . . . . . 14
4544eqeq1d 1925 . . . . . . . . . . . . 13
4645biimprd 211 . . . . . . . . . . . 12
4739, 46syl6 28 . . . . . . . . . . 11
4847exp3a 420 . . . . . . . . . 10
4948imp4a 565 . . . . . . . . 9
5049reximdvai 2226 . . . . . . . 8
5122, 50syld 39 . . . . . . 7
527, 51pm2.61dne 2107 . . . . . 6
5352ex 418 . . . . 5
5453exlimdv 1634 . . . 4
552, 54syl5bi 205 . . 3
561, 55syl6com 30 . 2
57563imp 1105 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 356   w3a 898  wex 1334   wceq 1413   wcel 1415   wne 2034  wral 2125  wrex 2126   cin 2631   wss 2632  c0 2898   cep 3606   wfr 3648   wwe 3649
This theorem is referenced by:  tz7.5 3700  finminlem 17805
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1330  ax-6 1331  ax-7 1332  ax-gen 1333  ax-8 1417  ax-10 1418  ax-11 1419  ax-12 1420  ax-14 1422  ax-17 1429  ax-9 1444  ax-4 1450  ax-16 1628  ax-ext 1899  ax-sep 3454  ax-nul 3463  ax-pr 3523
This theorem depends on definitions:  df-bi 174  df-or 357  df-an 358  df-3an 900  df-ex 1335  df-sb 1590  df-eu 1817  df-mo 1818  df-clab 1905  df-cleq 1910  df-clel 1913  df-ne 2036  df-ral 2129  df-rex 2130  df-v 2324  df-dif 2635  df-un 2637  df-in 2639  df-ss 2641  df-nul 2899  df-sn 3079  df-pr 3080  df-op 3082  df-br 3359  df-opab 3413  df-eprel 3608  df-po 3616  df-so 3630  df-fr 3650  df-we 3666
Copyright terms: Public domain