Theorem gruiun

Description: If B ( x ) is a family of elements of U and the index set A is an element of U , then the indexed union U_ x e. A B is also an element of U , where U is a Grothendieck universe. (Contributed by Mario Carneiro, 9-Jun-2013)

	Ref	Expression
Assertion	gruiun	|- ( ( U e. Univ /\ A e. U /\ A. x e. A B e. U ) -> U_ x e. A B e. U )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( x e. A |-> B ) = ( x e. A |-> B )
2	1	fnmpt	|- ( A. x e. A B e. U -> ( x e. A |-> B ) Fn A )
3	1	rnmptss	|- ( A. x e. A B e. U -> ran ( x e. A |-> B ) C_ U )
4		df-f	|- ( ( x e. A |-> B ) : A --> U <-> ( ( x e. A |-> B ) Fn A /\ ran ( x e. A |-> B ) C_ U ) )
5	2 3 4	sylanbrc	|- ( A. x e. A B e. U -> ( x e. A |-> B ) : A --> U )
6		gruurn	|- ( ( U e. Univ /\ A e. U /\ ( x e. A |-> B ) : A --> U ) -> U. ran ( x e. A |-> B ) e. U )
7	6	3expia	|- ( ( U e. Univ /\ A e. U ) -> ( ( x e. A |-> B ) : A --> U -> U. ran ( x e. A |-> B ) e. U ) )
8	5 7	syl5com	|- ( A. x e. A B e. U -> ( ( U e. Univ /\ A e. U ) -> U. ran ( x e. A |-> B ) e. U ) )
9		dfiun3g	|- ( A. x e. A B e. U -> U_ x e. A B = U. ran ( x e. A |-> B ) )
10	9	eleq1d	|- ( A. x e. A B e. U -> ( U_ x e. A B e. U <-> U. ran ( x e. A |-> B ) e. U ) )
11	8 10	sylibrd	|- ( A. x e. A B e. U -> ( ( U e. Univ /\ A e. U ) -> U_ x e. A B e. U ) )
12	11	com12	|- ( ( U e. Univ /\ A e. U ) -> ( A. x e. A B e. U -> U_ x e. A B e. U ) )
13	12	3impia	|- ( ( U e. Univ /\ A e. U /\ A. x e. A B e. U ) -> U_ x e. A B e. U )