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

Theorem r10 8226
Description: Value of the cumulative hierarchy of sets function at  (/). Part of Definition 9.9 of [TakeutiZaring] p. 76. (Contributed by NM, 2-Sep-2003.) (Revised by Mario Carneiro, 10-Sep-2013.)
Assertion
Ref Expression
r10  |-  ( R1
`  (/) )  =  (/)

Proof of Theorem r10
StepHypRef Expression
1 df-r1 8222 . . 3  |-  R1  =  rec ( ( x  e. 
_V  |->  ~P x ) ,  (/) )
21fveq1i 5849 . 2  |-  ( R1
`  (/) )  =  ( rec ( ( x  e.  _V  |->  ~P x
) ,  (/) ) `  (/) )
3 0ex 4507 . . 3  |-  (/)  e.  _V
43rdg0 7126 . 2  |-  ( rec ( ( x  e. 
_V  |->  ~P x ) ,  (/) ) `  (/) )  =  (/)
52, 4eqtri 2474 1  |-  ( R1
`  (/) )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1448   _Vcvv 3013   (/)c0 3699   ~Pcpw 3919    |-> cmpt 4433   ` cfv 5561   reccrdg 7114   R1cr1 8220
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-8 1893  ax-9 1900  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432  ax-sep 4497  ax-nul 4506  ax-pow 4554  ax-pr 4612  ax-un 6571
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 987  df-3an 988  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-eu 2304  df-mo 2305  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3015  df-sbc 3236  df-csb 3332  df-dif 3375  df-un 3377  df-in 3379  df-ss 3386  df-pss 3388  df-nul 3700  df-if 3850  df-pw 3921  df-sn 3937  df-pr 3939  df-tp 3941  df-op 3943  df-uni 4169  df-iun 4250  df-br 4375  df-opab 4434  df-mpt 4435  df-tr 4470  df-eprel 4723  df-id 4727  df-po 4733  df-so 4734  df-fr 4771  df-we 4773  df-xp 4818  df-rel 4819  df-cnv 4820  df-co 4821  df-dm 4822  df-rn 4823  df-res 4824  df-ima 4825  df-pred 5359  df-ord 5405  df-on 5406  df-lim 5407  df-suc 5408  df-iota 5525  df-fun 5563  df-fn 5564  df-f 5565  df-f1 5566  df-fo 5567  df-f1o 5568  df-fv 5569  df-om 6681  df-wrecs 7015  df-recs 7077  df-rdg 7115  df-r1 8222
This theorem is referenced by:  r1fin  8231  r1tr  8234  r1pwss  8242  r1val1  8244  rankeq0b  8318  ackbij2lem2  8657  ackbij2lem3  8658  wunr1om  9131  r1wunlim  9149  tskr1om  9179  inar1  9187  r1tskina  9194  grur1a  9231  grothomex  9241  rankeq1o  30944
  Copyright terms: Public domain W3C validator