This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem r1limg

Description: Value of the cumulative hierarchy of sets function at a limit ordinal. Part of Definition 9.9 of TakeutiZaring p. 76. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion r1limg 
|- ( ( A e. dom R1 /\ Lim A ) -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) )

Proof

Step Hyp Ref Expression
1 df-r1 
 |-  R1 = rec ( ( y e. _V |-> ~P y ) , (/) )
2 1 dmeqi 
 |-  dom R1 = dom rec ( ( y e. _V |-> ~P y ) , (/) )
3 2 eleq2i 
 |-  ( A e. dom R1 <-> A e. dom rec ( ( y e. _V |-> ~P y ) , (/) ) )
4 rdglimg 
 |-  ( ( A e. dom rec ( ( y e. _V |-> ~P y ) , (/) ) /\ Lim A ) -> ( rec ( ( y e. _V |-> ~P y ) , (/) ) ` A ) = U. ( rec ( ( y e. _V |-> ~P y ) , (/) ) " A ) )
5 3 4 sylanb 
 |-  ( ( A e. dom R1 /\ Lim A ) -> ( rec ( ( y e. _V |-> ~P y ) , (/) ) ` A ) = U. ( rec ( ( y e. _V |-> ~P y ) , (/) ) " A ) )
6 1 fveq1i 
 |-  ( R1 ` A ) = ( rec ( ( y e. _V |-> ~P y ) , (/) ) ` A )
7 r1funlim 
 |-  ( Fun R1 /\ Lim dom R1 )
8 7 simpli 
 |-  Fun R1
9 funiunfv 
 |-  ( Fun R1 -> U_ x e. A ( R1 ` x ) = U. ( R1 " A ) )
10 8 9 ax-mp 
 |-  U_ x e. A ( R1 ` x ) = U. ( R1 " A )
11 1 imaeq1i 
 |-  ( R1 " A ) = ( rec ( ( y e. _V |-> ~P y ) , (/) ) " A )
12 11 unieqi 
 |-  U. ( R1 " A ) = U. ( rec ( ( y e. _V |-> ~P y ) , (/) ) " A )
13 10 12 eqtri 
 |-  U_ x e. A ( R1 ` x ) = U. ( rec ( ( y e. _V |-> ~P y ) , (/) ) " A )
14 5 6 13 3eqtr4g 
 |-  ( ( A e. dom R1 /\ Lim A ) -> ( R1 ` A ) = U_ x e. A ( R1 ` x ) )