gruuni

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

		Ref	Expression
	Assertion	gruuni	$⊢ (U \in Univ \land A \in U) \to ⋃ A \in U$

Step	Hyp	Ref	Expression
1		uniiun	$⊢ ⋃ A = ⋃_{x \in A} x$
2		gruelss	$⊢ (U \in Univ \land A \in U) \to A \subseteq U$
3		dfss3	$⊢ A \subseteq U \leftrightarrow \forall x \in A x \in U$
4	2 3	sylib	$⊢ (U \in Univ \land A \in U) \to \forall x \in A x \in U$
5		gruiun	$⊢ (U \in Univ \land A \in U \land \forall x \in A x \in U) \to ⋃_{x \in A} x \in U$
6	4 5	mpd3an3	$⊢ (U \in Univ \land A \in U) \to ⋃_{x \in A} x \in U$
7	1 6	eqeltrid	$⊢ (U \in Univ \land A \in U) \to ⋃ A \in U$

Metamath Proof Explorer