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	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
2	1	fnmpt	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 )
3	1	rnmptss	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑈 )
4		df-f	⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝑈 ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ∧ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝑈 ) )
5	2 3 4	sylanbrc	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝑈 )
6		gruurn	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝑈 ) → ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑈 )
7	6	3expia	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ 𝑈 → ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑈 ) )
8	5 7	syl5com	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 → ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑈 ) )
9		dfiun3g	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 → ∪ 𝑥 ∈ 𝐴 𝐵 = ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) )
10	9	eleq1d	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 → ( ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ↔ ∪ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝑈 ) )
11	8 10	sylibrd	⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 → ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) )
12	11	com12	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) )
13	12	3impia	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 ) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝑈 )