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

Theorem wefrc 3713
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 3706 . . 3
2 n0 2916 . . . 4
3 ineq2 2823 . . . . . . . . . . 11
43eqeq1d 1926 . . . . . . . . . 10
54rcla4ev 2413 . . . . . . . . 9
65ex 419 . . . . . . . 8
76adantl 445 . . . . . . 7
8 inss1 2847 . . . . . . . . . . 11
9 wefr 3709 . . . . . . . . . . . . 13
10 vex 2330 . . . . . . . . . . . . . . 15
1110inex2 3507 . . . . . . . . . . . . . 14
1211epfrc 3704 . . . . . . . . . . . . 13
139, 12syl3an1 1175 . . . . . . . . . . . 12
14133exp 1111 . . . . . . . . . . 11
158, 14mpi 16 . . . . . . . . . 10
16 elin 2819 . . . . . . . . . . . . 13
1716anbi1i 672 . . . . . . . . . . . 12
18 anass 625 . . . . . . . . . . . 12
1917, 18bitri 238 . . . . . . . . . . 11
2019rexbii2 2154 . . . . . . . . . 10
2115, 20syl6ib 215 . . . . . . . . 9
2221adantr 444 . . . . . . . 8
23 elin 2819 . . . . . . . . . . . . . . . . 17
24 df-3an 901 . . . . . . . . . . . . . . . . . . . . . . 23
25 3anrot 904 . . . . . . . . . . . . . . . . . . . . . . 23
2624, 25bitr3i 240 . . . . . . . . . . . . . . . . . . . . . 22
27 wetrep 3712 . . . . . . . . . . . . . . . . . . . . . . 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 2652 . . . . . . . . . . . . 13
3937, 38syl6ibr 216 . . . . . . . . . . . 12
40 dfss 2649 . . . . . . . . . . . . . . . 16
41 in32 2839 . . . . . . . . . . . . . . . . 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 2636   wss 2637  c0 2907   cep 3644   wfr 3687   wwe 3688
This theorem is referenced by:  tz7.5 3739  finminlem 19196
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 3491  ax-nul 3500  ax-pr 3560
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-rab 2134  df-v 2329  df-dif 2640  df-un 2642  df-in 2644  df-ss 2648  df-nul 2908  df-if 3015  df-sn 3092  df-pr 3093  df-op 3095  df-br 3397  df-opab 3450  df-eprel 3646  df-po 3655  df-so 3669  df-fr 3689  df-we 3705
Copyright terms: Public domain