Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  wfrlem10 Structured version   Unicode version

Theorem wfrlem10 7000
 Description: Lemma for well-founded recursion. When is an minimal element of , then its predecessor class is equal to . (Contributed by Scott Fenton, 21-Apr-2011.)
Hypotheses
Ref Expression
wfrlem10.1
wfrlem10.2 wrecs
Assertion
Ref Expression
wfrlem10
Distinct variable group:   ,
Allowed substitution hints:   ()   ()   ()

Proof of Theorem wfrlem10
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 wfrlem10.2 . . . 4 wrecs
21wfrlem8 6998 . . 3
32biimpi 197 . 2
4 predss 5349 . . . 4
54a1i 11 . . 3
6 simpr 462 . . . . . 6
7 eldifn 3531 . . . . . . . . . 10
8 eleq1 2494 . . . . . . . . . . 11
98notbid 295 . . . . . . . . . 10
107, 9syl5ibrcom 225 . . . . . . . . 9
1110con2d 118 . . . . . . . 8
1211imp 430 . . . . . . 7
131wfrdmcl 6999 . . . . . . . . . 10
1413adantl 467 . . . . . . . . 9
15 ssel 3401 . . . . . . . . . . . 12
1615con3d 138 . . . . . . . . . . 11
177, 16syl5com 31 . . . . . . . . . 10
1817adantr 466 . . . . . . . . 9
1914, 18mpd 15 . . . . . . . 8
20 eldifi 3530 . . . . . . . . 9
21 elpredg 5356 . . . . . . . . . 10
2221ancoms 454 . . . . . . . . 9
2320, 22sylan 473 . . . . . . . 8
2419, 23mtbid 301 . . . . . . 7
251wfrdmss 6997 . . . . . . . . 9
2625sseli 3403 . . . . . . . 8
27 wfrlem10.1 . . . . . . . . . 10
28 weso 4787 . . . . . . . . . 10
2927, 28ax-mp 5 . . . . . . . . 9
30 solin 4740 . . . . . . . . 9
3129, 30mpan 674 . . . . . . . 8
3226, 20, 31syl2anr 480 . . . . . . 7
3312, 24, 32ecase23d 1368 . . . . . 6
34 vex 3025 . . . . . . 7
35 vex 3025 . . . . . . . 8
3635elpred 5355 . . . . . . 7
3734, 36ax-mp 5 . . . . . 6
386, 33, 37sylanbrc 668 . . . . 5
3938ex 435 . . . 4
4039ssrdv 3413 . . 3
415, 40eqssd 3424 . 2
423, 41sylan9eqr 2484 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   w3o 981   wceq 1437   wcel 1872  cvv 3022   cdif 3376   wss 3379  c0 3704   class class class wbr 4366   wor 4716   wwe 4754   cdm 4796  cpred 5341  wrecscwrecs 6982 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-sep 4489  ax-nul 4498  ax-pr 4603 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-ral 2719  df-rex 2720  df-rab 2723  df-v 3024  df-sbc 3243  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-nul 3705  df-if 3855  df-sn 3942  df-pr 3944  df-op 3948  df-uni 4163  df-iun 4244  df-br 4367  df-opab 4426  df-so 4718  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-iota 5508  df-fun 5546  df-fn 5547  df-fv 5552  df-wrecs 6983 This theorem is referenced by:  wfrlem15  7005
 Copyright terms: Public domain W3C validator