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

Theorem unwf 8233
 Description: A binary union is well-founded iff its elements are. (Contributed by Mario Carneiro, 10-Jun-2013.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
unwf

Proof of Theorem unwf
StepHypRef Expression
1 r1rankidb 8227 . . . . . . . 8
21adantr 466 . . . . . . 7
3 ssun1 3572 . . . . . . . 8
4 rankdmr1 8224 . . . . . . . . 9
5 r1funlim 8189 . . . . . . . . . . . 12
65simpri 463 . . . . . . . . . . 11
7 limord 5444 . . . . . . . . . . 11
86, 7ax-mp 5 . . . . . . . . . 10
9 rankdmr1 8224 . . . . . . . . . 10
10 ordunel 6612 . . . . . . . . . 10
118, 4, 9, 10mp3an 1360 . . . . . . . . 9
12 r1ord3g 8202 . . . . . . . . 9
134, 11, 12mp2an 676 . . . . . . . 8
143, 13ax-mp 5 . . . . . . 7
152, 14syl6ss 3419 . . . . . 6
16 r1rankidb 8227 . . . . . . . 8
1716adantl 467 . . . . . . 7
18 ssun2 3573 . . . . . . . 8
19 r1ord3g 8202 . . . . . . . . 9
209, 11, 19mp2an 676 . . . . . . . 8
2118, 20ax-mp 5 . . . . . . 7
2217, 21syl6ss 3419 . . . . . 6
2315, 22unssd 3585 . . . . 5
24 fvex 5835 . . . . . 6
2524elpw2 4531 . . . . 5
2623, 25sylibr 215 . . . 4
27 r1sucg 8192 . . . . 5
2811, 27ax-mp 5 . . . 4
2926, 28syl6eleqr 2517 . . 3
30 r1elwf 8219 . . 3
3129, 30syl 17 . 2
32 ssun1 3572 . . . 4
33 sswf 8231 . . . 4
3432, 33mpan2 675 . . 3
35 ssun2 3573 . . . 4
36 sswf 8231 . . . 4
3735, 36mpan2 675 . . 3
3834, 37jca 534 . 2
3931, 38impbii 190 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wb 187   wa 370   wceq 1437   wcel 1872   cun 3377   wss 3379  cpw 3924  cuni 4162   cdm 4796  cima 4799   word 5384  con0 5385   wlim 5386   csuc 5387   wfun 5538  cfv 5544  cr1 8185  crnk 8186 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-8 1874  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-pow 4545  ax-pr 4603  ax-un 6541 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-reu 2721  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  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-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-om 6651  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-r1 8187  df-rank 8188 This theorem is referenced by:  prwf  8234  rankunb  8273
 Copyright terms: Public domain W3C validator