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

Theorem rankuni2b 7733
 Description: The value of the rank function expressed recursively: the rank of a set is the smallest ordinal number containing the ranks of all members of the set. Proposition 9.17 of [TakeutiZaring] p. 79. (Contributed by Mario Carneiro, 8-Jun-2013.)
Assertion
Ref Expression
rankuni2b
Distinct variable group:   ,

Proof of Theorem rankuni2b
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 uniwf 7699 . . . 4
2 rankval3b 7706 . . . 4
31, 2sylbi 188 . . 3
4 iuneq1 4064 . . . . . . 7
54eleq1d 2468 . . . . . 6
6 vex 2917 . . . . . . 7
7 rankon 7675 . . . . . . . 8
87rgenw 2731 . . . . . . 7
9 iunon 6557 . . . . . . 7
106, 8, 9mp2an 654 . . . . . 6
115, 10vtoclg 2969 . . . . 5
12 eluni2 3977 . . . . . . 7
13 nfv 1626 . . . . . . . 8
14 nfiu1 4079 . . . . . . . . 9
1514nfel2 2550 . . . . . . . 8
16 r1elssi 7685 . . . . . . . . . . 11
1716sseld 3305 . . . . . . . . . 10
18 rankelb 7704 . . . . . . . . . 10
1917, 18syl6 31 . . . . . . . . 9
20 ssiun2 4092 . . . . . . . . . . 11
2120sseld 3305 . . . . . . . . . 10
2221a1i 11 . . . . . . . . 9
2319, 22syldd 63 . . . . . . . 8
2413, 15, 23rexlimd 2785 . . . . . . 7
2512, 24syl5bi 209 . . . . . 6
2625ralrimiv 2746 . . . . 5
27 eleq2 2463 . . . . . . 7
2827ralbidv 2684 . . . . . 6
2928elrab 3050 . . . . 5
3011, 26, 29sylanbrc 646 . . . 4
31 intss1 4023 . . . 4
3230, 31syl 16 . . 3
333, 32eqsstrd 3340 . 2
341biimpi 187 . . . . 5
35 elssuni 4001 . . . . 5
36 rankssb 7728 . . . . 5
3734, 35, 36syl2im 36 . . . 4
3837ralrimiv 2746 . . 3
39 iunss 4090 . . 3
4038, 39sylibr 204 . 2
4133, 40eqssd 3323 1
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1649   wcel 1721  wral 2664  wrex 2665  crab 2668  cvv 2914   wss 3278  cuni 3973  cint 4008  ciun 4051  con0 4539  cima 4838  cfv 5411  cr1 7642  crnk 7643 This theorem is referenced by:  rankuni2  7735  rankcf  8606 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2383  ax-rep 4278  ax-sep 4288  ax-nul 4296  ax-pow 4335  ax-pr 4361  ax-un 4658 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2256  df-mo 2257  df-clab 2389  df-cleq 2395  df-clel 2398  df-nfc 2527  df-ne 2567  df-ral 2669  df-rex 2670  df-reu 2671  df-rab 2673  df-v 2916  df-sbc 3120  df-csb 3210  df-dif 3281  df-un 3283  df-in 3285  df-ss 3292  df-pss 3294  df-nul 3587  df-if 3698  df-pw 3759  df-sn 3778  df-pr 3779  df-tp 3780  df-op 3781  df-uni 3974  df-int 4009  df-iun 4053  df-br 4171  df-opab 4225  df-mpt 4226  df-tr 4261  df-eprel 4452  df-id 4456  df-po 4461  df-so 4462  df-fr 4499  df-we 4501  df-ord 4542  df-on 4543  df-lim 4544  df-suc 4545  df-om 4803  df-xp 4841  df-rel 4842  df-cnv 4843  df-co 4844  df-dm 4845  df-rn 4846  df-res 4847  df-ima 4848  df-iota 5375  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-recs 6590  df-rdg 6625  df-r1 7644  df-rank 7645
 Copyright terms: Public domain W3C validator