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

Theorem wefrc 3673
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 3666 . . 3
2 n0 2908 . . . 4
3 ineq2 2816 . . . . . . . . . . 11
43eqeq1d 1937 . . . . . . . . . 10
54rcla4ev 2421 . . . . . . . . 9
65ex 423 . . . . . . . 8
76adantl 449 . . . . . . 7
8 inss1 2839 . . . . . . . . . . 11
9 wefr 3669 . . . . . . . . . . . . 13
10 vex 2338 . . . . . . . . . . . . . . 15
1110inex2 3470 . . . . . . . . . . . . . 14
1211epfrc 3664 . . . . . . . . . . . . 13
139, 12syl3an1 1186 . . . . . . . . . . . 12
14133exp 1122 . . . . . . . . . . 11
158, 14mpi 15 . . . . . . . . . 10
16 elin 2812 . . . . . . . . . . . . 13
1716anbi1i 677 . . . . . . . . . . . 12
18 anass 629 . . . . . . . . . . . 12
1917, 18bitri 239 . . . . . . . . . . 11
2019rexbii2 2165 . . . . . . . . . 10
2115, 20syl6ib 216 . . . . . . . . 9
2221adantr 448 . . . . . . . 8
23 elin 2812 . . . . . . . . . . . . . . . . 17
24 df-3an 914 . . . . . . . . . . . . . . . . . . . . . . 23
25 3anrot 917 . . . . . . . . . . . . . . . . . . . . . . 23
2624, 25bitr3i 241 . . . . . . . . . . . . . . . . . . . . . 22
27 wetrep 3672 . . . . . . . . . . . . . . . . . . . . . . 23
2827exp3a 425 . . . . . . . . . . . . . . . . . . . . . 22
2926, 28sylan2b 458 . . . . . . . . . . . . . . . . . . . . 21
3029exp44 594 . . . . . . . . . . . . . . . . . . . 20
3130imp 418 . . . . . . . . . . . . . . . . . . 19
3231com34 76 . . . . . . . . . . . . . . . . . 18
3332imp3a 420 . . . . . . . . . . . . . . . . 17
3423, 33syl5bi 206 . . . . . . . . . . . . . . . 16
3534imp4a 570 . . . . . . . . . . . . . . 15
3635com23 71 . . . . . . . . . . . . . 14
3736ralrimdv 2218 . . . . . . . . . . . . 13
38 dfss3 2649 . . . . . . . . . . . . 13
3937, 38syl6ibr 217 . . . . . . . . . . . 12
40 dfss 2644 . . . . . . . . . . . . . . . 16
41 in32 2831 . . . . . . . . . . . . . . . . 17
4241eqeq2i 1939 . . . . . . . . . . . . . . . 16
4340, 42bitri 239 . . . . . . . . . . . . . . 15
4443biimpi 184 . . . . . . . . . . . . . 14
4544eqeq1d 1937 . . . . . . . . . . . . 13
4645biimprd 212 . . . . . . . . . . . 12
4739, 46syl6 28 . . . . . . . . . . 11
4847exp3a 425 . . . . . . . . . 10
4948imp4a 570 . . . . . . . . 9
5049reximdvai 2239 . . . . . . . 8
5122, 50syld 39 . . . . . . 7
527, 51pm2.61dne 2120 . . . . . 6
5352ex 423 . . . . 5
5453exlimdv 1646 . . . 4
552, 54syl5bi 206 . . 3
561, 55syl6com 30 . 2
57563imp 1117 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 360   w3a 912  wex 1346   wceq 1425   wcel 1427   wne 2047  wral 2138  wrex 2139   cin 2633   wss 2634  c0 2899   cep 3606   wfr 3647   wwe 3648
This theorem is referenced by:  tz7.5 3699  finminlem 16889
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-5 1342  ax-6 1343  ax-7 1344  ax-gen 1345  ax-8 1429  ax-10 1430  ax-11 1431  ax-12 1432  ax-14 1434  ax-17 1441  ax-9 1456  ax-4 1462  ax-16 1640  ax-ext 1911  ax-sep 3454  ax-nul 3463  ax-pr 3523
This theorem depends on definitions:  df-bi 175  df-or 361  df-an 362  df-3an 914  df-ex 1347  df-sb 1602  df-eu 1829  df-mo 1830  df-clab 1917  df-cleq 1922  df-clel 1925  df-ne 2049  df-ral 2142  df-rex 2143  df-v 2337  df-dif 2637  df-un 2639  df-in 2641  df-ss 2643  df-nul 2900  df-sn 3080  df-pr 3081  df-op 3083  df-br 3359  df-opab 3413  df-eprel 3608  df-po 3616  df-so 3630  df-fr 3649  df-we 3665
Copyright terms: Public domain