Theorem gruuni

Description: A Grothendieck universe contains unions of its elements. (Contributed by Mario Carneiro, 17-Jun-2013)

	Ref	Expression
Assertion	gruuni	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ∪ 𝐴 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		uniiun	⊢ ∪ 𝐴 = ∪ 𝑥 ∈ 𝐴 𝑥
2		gruelss	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → 𝐴 ⊆ 𝑈 )
3		dfss3	⊢ ( 𝐴 ⊆ 𝑈 ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝑈 )
4	2 3	sylib	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝑈 )
5		gruiun	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ∀ 𝑥 ∈ 𝐴 𝑥 ∈ 𝑈 ) → ∪ 𝑥 ∈ 𝐴 𝑥 ∈ 𝑈 )
6	4 5	mpd3an3	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ∪ 𝑥 ∈ 𝐴 𝑥 ∈ 𝑈 )
7	1 6	eqeltrid	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) → ∪ 𝐴 ∈ 𝑈 )