Metamath Proof Explorer

Theorem gruurn

Description: A Grothendieck universe contains the range of any function which takes values in the universe (see gruiun for a more intuitive version). (Contributed by Mario Carneiro, 9-Jun-2013)

		Ref	Expression
	Assertion	gruurn	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to ⋃ ran F \in U$

Proof

Step	Hyp	Ref	Expression
1		elmapg	$⊢ (U \in Univ \land A \in U) \to (F \in (U^{A}) \leftrightarrow F : A ⟶ U)$
2		elgrug	$⊢ U \in Univ \to (U \in Univ \leftrightarrow (Tr U \land \forall x \in U (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U)))$
3	2	ibi	$⊢ U \in Univ \to (Tr U \land \forall x \in U (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U))$
4	3	simprd	$⊢ U \in Univ \to \forall x \in U (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U)$
5		rneq	$⊢ y = F \to ran y = ran F$
6	5	unieqd	$⊢ y = F \to ⋃ ran y = ⋃ ran F$
7	6	eleq1d	$⊢ y = F \to (⋃ ran y \in U \leftrightarrow ⋃ ran F \in U)$
8	7	rspccv	$⊢ \forall y \in (U^{x}) ⋃ ran y \in U \to (F \in (U^{x}) \to ⋃ ran F \in U)$
9	8	3ad2ant3	$⊢ (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U) \to (F \in (U^{x}) \to ⋃ ran F \in U)$
10	9	ralimi	$⊢ \forall x \in U (𝒫 x \in U \land \forall y \in U \{x, y\} \in U \land \forall y \in (U^{x}) ⋃ ran y \in U) \to \forall x \in U (F \in (U^{x}) \to ⋃ ran F \in U)$
11		oveq2	$⊢ x = A \to U^{x} = U^{A}$
12	11	eleq2d	$⊢ x = A \to (F \in (U^{x}) \leftrightarrow F \in (U^{A}))$
13	12	imbi1d	$⊢ x = A \to ((F \in (U^{x}) \to ⋃ ran F \in U) \leftrightarrow (F \in (U^{A}) \to ⋃ ran F \in U))$
14	13	rspccv	$⊢ \forall x \in U (F \in (U^{x}) \to ⋃ ran F \in U) \to (A \in U \to (F \in (U^{A}) \to ⋃ ran F \in U))$
15	4 10 14	3syl	$⊢ U \in Univ \to (A \in U \to (F \in (U^{A}) \to ⋃ ran F \in U))$
16	15	imp	$⊢ (U \in Univ \land A \in U) \to (F \in (U^{A}) \to ⋃ ran F \in U)$
17	1 16	sylbird	$⊢ (U \in Univ \land A \in U) \to (F : A ⟶ U \to ⋃ ran F \in U)$
18	17	3impia	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to ⋃ ran F \in U$