Theorem itunifval

Description: Function value of iterated unions.EDITORIAL: The iterated unions and order types of ordered sets are split out here because they could conceivably be independently useful. (Contributed by Stefan O'Rear, 11-Feb-2015)

	Ref	Expression
Hypothesis	ituni.u	|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) )
Assertion	itunifval	|- ( A e. V -> ( U ` A ) = ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) )

Proof

Step	Hyp	Ref	Expression
1		ituni.u	|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) )
2		elex	|- ( A e. V -> A e. _V )
3		rdgeq2	|- ( x = A -> rec ( ( y e. _V |-> U. y ) , x ) = rec ( ( y e. _V |-> U. y ) , A ) )
4	3	reseq1d	|- ( x = A -> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) = ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) )
5		rdgfun	|- Fun rec ( ( y e. _V |-> U. y ) , A )
6		omex	|- _om e. _V
7		resfunexg	|- ( ( Fun rec ( ( y e. _V |-> U. y ) , A ) /\ _om e. _V ) -> ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) e. _V )
8	5 6 7	mp2an	|- ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) e. _V
9	4 1 8	fvmpt	|- ( A e. _V -> ( U ` A ) = ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) )
10	2 9	syl	|- ( A e. V -> ( U ` A ) = ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) )