Theorem itunifn

Description: Functionality of the iterated union. (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	itunifn	|- ( A e. V -> ( U ` A ) Fn _om )

Proof

Step	Hyp	Ref	Expression
1		ituni.u	|- U = ( x e. _V |-> ( rec ( ( y e. _V |-> U. y ) , x ) |` _om ) )
2		frfnom	|- ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) Fn _om
3	1	itunifval	|- ( A e. V -> ( U ` A ) = ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) )
4	3	fneq1d	|- ( A e. V -> ( ( U ` A ) Fn _om <-> ( rec ( ( y e. _V |-> U. y ) , A ) |` _om ) Fn _om ) )
5	2 4	mpbiri	|- ( A e. V -> ( U ` A ) Fn _om )