Metamath Proof Explorer

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 \in Univ \land A \in U \land \forall x \in A B \in U) \to ⋃_{x \in A} B \in U$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ (x \in A ⟼ B) = (x \in A ⟼ B)$
2	1	fnmpt	$⊢ \forall x \in A B \in U \to (x \in A ⟼ B) Fn A$
3	1	rnmptss	$⊢ \forall x \in A B \in U \to ran (x \in A ⟼ B) \subseteq U$
4		df-f	$⊢ (x \in A ⟼ B) : A ⟶ U \leftrightarrow ((x \in A ⟼ B) Fn A \land ran (x \in A ⟼ B) \subseteq U)$
5	2 3 4	sylanbrc	$⊢ \forall x \in A B \in U \to (x \in A ⟼ B) : A ⟶ U$
6		gruurn	$⊢ (U \in Univ \land A \in U \land (x \in A ⟼ B) : A ⟶ U) \to ⋃ ran (x \in A ⟼ B) \in U$
7	6	3expia	$⊢ (U \in Univ \land A \in U) \to ((x \in A ⟼ B) : A ⟶ U \to ⋃ ran (x \in A ⟼ B) \in U)$
8	5 7	syl5com	$⊢ \forall x \in A B \in U \to ((U \in Univ \land A \in U) \to ⋃ ran (x \in A ⟼ B) \in U)$
9		dfiun3g	$⊢ \forall x \in A B \in U \to ⋃_{x \in A} B = ⋃ ran (x \in A ⟼ B)$
10	9	eleq1d	$⊢ \forall x \in A B \in U \to (⋃_{x \in A} B \in U \leftrightarrow ⋃ ran (x \in A ⟼ B) \in U)$
11	8 10	sylibrd	$⊢ \forall x \in A B \in U \to ((U \in Univ \land A \in U) \to ⋃_{x \in A} B \in U)$
12	11	com12	$⊢ (U \in Univ \land A \in U) \to (\forall x \in A B \in U \to ⋃_{x \in A} B \in U)$
13	12	3impia	$⊢ (U \in Univ \land A \in U \land \forall x \in A B \in U) \to ⋃_{x \in A} B \in U$