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

Theorem wefrc 3686
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 3679 . . 3
2 n0 2911 . . . 4
3 ineq2 2818 . . . . . . . . . . 11
43eqeq1d 1926 . . . . . . . . . 10
54rcla4ev 2410 . . . . . . . . 9
65ex 419 . . . . . . . 8
76adantl 445 . . . . . . 7
8 inss1 2842 . . . . . . . . . . 11
9 wefr 3682 . . . . . . . . . . . . 13
10 vex 2327 . . . . . . . . . . . . . . 15
1110inex2 3482 . . . . . . . . . . . . . 14
1211epfrc 3677 . . . . . . . . . . . . 13
139, 12syl3an1 1175 . . . . . . . . . . . 12
14133exp 1111 . . . . . . . . . . 11
158, 14mpi 16 . . . . . . . . . 10
16 elin 2814 . . . . . . . . . . . . 13
1716anbi1i 672 . . . . . . . . . . . 12
18 anass 625 . . . . . . . . . . . 12
1917, 18bitri 238 . . . . . . . . . . 11
2019rexbii2 2154 . . . . . . . . . 10
2115, 20syl6ib 215 . . . . . . . . 9
2221adantr 444 . . . . . . . 8
23 elin 2814 . . . . . . . . . . . . . . . . 17
24 df-3an 901 . . . . . . . . . . . . . . . . . . . . . . 23
25 3anrot 904 . . . . . . . . . . . . . . . . . . . . . . 23
2624, 25bitr3i 240 . . . . . . . . . . . . . . . . . . . . . 22
27 wetrep 3685 . . . . . . . . . . . . . . . . . . . . . . 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 2649 . . . . . . . . . . . . 13
3937, 38syl6ibr 216 . . . . . . . . . . . 12
40 dfss 2646 . . . . . . . . . . . . . . . 16
41 in32 2834 . . . . . . . . . . . . . . . . 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 2633   wss 2634  c0 2902   cep 3618   wfr 3660   wwe 3661
This theorem is referenced by:  tz7.5 3712  finminlem 18143
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 3466  ax-nul 3475  ax-pr 3535
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 2326  df-dif 2637  df-un 2639  df-in 2641  df-ss 2645  df-nul 2903  df-sn 3085  df-pr 3086  df-op 3088  df-br 3371  df-opab 3425  df-eprel 3620  df-po 3628  df-so 3642  df-fr 3662  df-we 3678
Copyright terms: Public domain