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

Theorem wefrc 3700
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 3693 . . 3
2 n0 2913 . . . 4
3 ineq2 2820 . . . . . . . . . . 11
43eqeq1d 1926 . . . . . . . . . 10
54rcla4ev 2412 . . . . . . . . 9
65ex 419 . . . . . . . 8
76adantl 445 . . . . . . 7
8 inss1 2844 . . . . . . . . . . 11
9 wefr 3696 . . . . . . . . . . . . 13
10 vex 2329 . . . . . . . . . . . . . . 15
1110inex2 3495 . . . . . . . . . . . . . 14
1211epfrc 3691 . . . . . . . . . . . . 13
139, 12syl3an1 1175 . . . . . . . . . . . 12
14133exp 1111 . . . . . . . . . . 11
158, 14mpi 16 . . . . . . . . . 10
16 elin 2816 . . . . . . . . . . . . 13
1716anbi1i 672 . . . . . . . . . . . 12
18 anass 625 . . . . . . . . . . . 12
1917, 18bitri 238 . . . . . . . . . . 11
2019rexbii2 2154 . . . . . . . . . 10
2115, 20syl6ib 215 . . . . . . . . 9
2221adantr 444 . . . . . . . 8
23 elin 2816 . . . . . . . . . . . . . . . . 17
24 df-3an 901 . . . . . . . . . . . . . . . . . . . . . . 23
25 3anrot 904 . . . . . . . . . . . . . . . . . . . . . . 23
2624, 25bitr3i 240 . . . . . . . . . . . . . . . . . . . . . 22
27 wetrep 3699 . . . . . . . . . . . . . . . . . . . . . . 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 2207 . . . . . . . . . . . . 13
38 dfss3 2651 . . . . . . . . . . . . 13
3937, 38syl6ibr 216 . . . . . . . . . . . 12
40 dfss 2648 . . . . . . . . . . . . . . . 16
41 in32 2836 . . . . . . . . . . . . . . . . 17
4241eqeq2i 1928 . . . . . . . . . . . . . . . 16
4340, 42bitri 238 . . . . . . . . . . . . . . 15
4443biimpi 184 . . . . . . . . . . . . . 14
4544eqeq1d 1926 . . . . . . . . . . . . 13
4645biimprd 212 . . . . . . . . . . . 12
4739, 46syl6 29 . . . . . . . . . . 11
4847exp3a 421 . . . . . . . . . 10
4948imp4a 566 . . . . . . . . 9
5049reximdvai 2228 . . . . . . . 8
5122, 50syld 40 . . . . . . 7
527, 51pm2.61dne 2109 . . . . . 6
5352ex 419 . . . . 5
5453exlimdv 1635 . . . 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 1335   wceq 1414   wcel 1416   wne 2035  wral 2127  wrex 2128   cin 2635   wss 2636  c0 2904   cep 3632   wfr 3674   wwe 3675
This theorem is referenced by:  tz7.5 3726  finminlem 18884
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1331  ax-6 1332  ax-7 1333  ax-gen 1334  ax-8 1418  ax-10 1419  ax-11 1420  ax-12 1421  ax-14 1423  ax-17 1430  ax-9 1445  ax-4 1451  ax-16 1629  ax-ext 1900  ax-sep 3479  ax-nul 3488  ax-pr 3548
This theorem depends on definitions:  df-bi 175  df-or 358  df-an 359  df-3an 901  df-ex 1336  df-sb 1591  df-eu 1818  df-mo 1819  df-clab 1906  df-cleq 1911  df-clel 1914  df-ne 2037  df-ral 2131  df-rex 2132  df-v 2328  df-dif 2639  df-un 2641  df-in 2643  df-ss 2647  df-nul 2905  df-sn 3089  df-pr 3090  df-op 3092  df-br 3384  df-opab 3438  df-eprel 3634  df-po 3642  df-so 3656  df-fr 3676  df-we 3692
Copyright terms: Public domain