Metamath Proof Explorer

Theorem grurn

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	grurn	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to ran F \in U$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to U \in Univ$
2		gruurn	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to ⋃ ran F \in U$
3		grupw	$⊢ (U \in Univ \land ⋃ ran F \in U) \to 𝒫 ⋃ ran F \in U$
4	1 2 3	syl2anc	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to 𝒫 ⋃ ran F \in U$
5		pwuni	$⊢ ran F \subseteq 𝒫 ⋃ ran F$
6	5	a1i	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to ran F \subseteq 𝒫 ⋃ ran F$
7		gruss	$⊢ (U \in Univ \land 𝒫 ⋃ ran F \in U \land ran F \subseteq 𝒫 ⋃ ran F) \to ran F \in U$
8	1 4 6 7	syl3anc	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to ran F \in U$