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 ) )