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

Theorem r1wunlim 8446
 Description: The weak universes in the cumulative hierarchy are exactly the limit ordinals. (Contributed by Mario Carneiro, 2-Jan-2017.)
Assertion
Ref Expression
r1wunlim WUni

Proof of Theorem r1wunlim
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 simpr 447 . . . . . . 7 WUni WUni
21wun0 8427 . . . . . 6 WUni
3 elfvdm 5634 . . . . . 6
42, 3syl 15 . . . . 5 WUni
5 r1fnon 7526 . . . . . 6
6 fndm 5422 . . . . . 6
75, 6ax-mp 8 . . . . 5
84, 7syl6eleq 2448 . . . 4 WUni
9 eloni 4481 . . . 4
108, 9syl 15 . . 3 WUni
11 n0i 3536 . . . . . 6
122, 11syl 15 . . . . 5 WUni
13 fveq2 5605 . . . . . 6
14 r10 7527 . . . . . 6
1513, 14syl6eq 2406 . . . . 5
1612, 15nsyl 113 . . . 4 WUni
17 suceloni 4683 . . . . . . . 8
188, 17syl 15 . . . . . . 7 WUni
19 sucidg 4549 . . . . . . . 8
208, 19syl 15 . . . . . . 7 WUni
21 r1ord 7539 . . . . . . 7
2218, 20, 21sylc 56 . . . . . 6 WUni
23 r1elwf 7555 . . . . . 6
24 wfelirr 7584 . . . . . 6
2522, 23, 243syl 18 . . . . 5 WUni
26 simprr 733 . . . . . . . . . 10 WUni
2726fveq2d 5609 . . . . . . . . 9 WUni
28 r1suc 7529 . . . . . . . . . 10
2928ad2antrl 708 . . . . . . . . 9 WUni
3027, 29eqtrd 2390 . . . . . . . 8 WUni
31 simplr 731 . . . . . . . . 9 WUni WUni
328adantr 451 . . . . . . . . . 10 WUni
33 sucidg 4549 . . . . . . . . . . . 12
3433ad2antrl 708 . . . . . . . . . . 11 WUni
3534, 26eleqtrrd 2435 . . . . . . . . . 10 WUni
36 r1ord 7539 . . . . . . . . . 10
3732, 35, 36sylc 56 . . . . . . . . 9 WUni
3831, 37wunpw 8416 . . . . . . . 8 WUni
3930, 38eqeltrd 2432 . . . . . . 7 WUni
4039expr 598 . . . . . 6 WUni
4140rexlimdva 2743 . . . . 5 WUni
4225, 41mtod 168 . . . 4 WUni
43 ioran 476 . . . 4
4416, 42, 43sylanbrc 645 . . 3 WUni
45 dflim3 4717 . . 3
4610, 44, 45sylanbrc 645 . 2 WUni
47 r1limwun 8445 . 2 WUni
4846, 47impbida 805 1 WUni
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 176   wo 357   wa 358   wceq 1642   wcel 1710  wrex 2620  c0 3531  cpw 3701  cuni 3906   word 4470  con0 4471   wlim 4472   csuc 4473   cdm 4768  cima 4771   wfn 5329  cfv 5334  cr1 7521  WUnicwun 8409 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-rep 4210  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-reg 7393  ax-inf2 7429 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3907  df-int 3942  df-iun 3986  df-br 4103  df-opab 4157  df-mpt 4158  df-tr 4193  df-eprel 4384  df-id 4388  df-po 4393  df-so 4394  df-fr 4431  df-we 4433  df-ord 4474  df-on 4475  df-lim 4476  df-suc 4477  df-om 4736  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-f1 5339  df-fo 5340  df-f1o 5341  df-fv 5342  df-recs 6472  df-rdg 6507  df-r1 7523  df-rank 7524  df-wun 8411
 Copyright terms: Public domain W3C validator