gruf

Description: A Grothendieck universe contains all functions on its elements. (Contributed by Mario Carneiro, 10-Jun-2013)

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

Step	Hyp	Ref	Expression
1		simp3	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to F : A ⟶ U$
2	1	feqmptd	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to F = (x \in A ⟼ F (x))$
3		fvex	$⊢ F (x) \in V$
4	3	fnasrn	$⊢ (x \in A ⟼ F (x)) = ran (x \in A ⟼ ⟨x, F (x)⟩)$
5	2 4	eqtrdi	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to F = ran (x \in A ⟼ ⟨x, F (x)⟩)$
6		simpl1	$⊢ ((U \in Univ \land A \in U \land F : A ⟶ U) \land x \in A) \to U \in Univ$
7		gruel	$⊢ (U \in Univ \land A \in U \land x \in A) \to x \in U$
8	7	3expa	$⊢ ((U \in Univ \land A \in U) \land x \in A) \to x \in U$
9	8	3adantl3	$⊢ ((U \in Univ \land A \in U \land F : A ⟶ U) \land x \in A) \to x \in U$
10		ffvelcdm	$⊢ (F : A ⟶ U \land x \in A) \to F (x) \in U$
11	10	3ad2antl3	$⊢ ((U \in Univ \land A \in U \land F : A ⟶ U) \land x \in A) \to F (x) \in U$
12		gruop	$⊢ (U \in Univ \land x \in U \land F (x) \in U) \to ⟨x, F (x)⟩ \in U$
13	6 9 11 12	syl3anc	$⊢ ((U \in Univ \land A \in U \land F : A ⟶ U) \land x \in A) \to ⟨x, F (x)⟩ \in U$
14	13	fmpttd	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to (x \in A ⟼ ⟨x, F (x)⟩) : A ⟶ U$
15		grurn	$⊢ (U \in Univ \land A \in U \land (x \in A ⟼ ⟨x, F (x)⟩) : A ⟶ U) \to ran (x \in A ⟼ ⟨x, F (x)⟩) \in U$
16	14 15	syld3an3	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to ran (x \in A ⟼ ⟨x, F (x)⟩) \in U$
17	5 16	eqeltrd	$⊢ (U \in Univ \land A \in U \land F : A ⟶ U) \to F \in U$

Metamath Proof Explorer