Theorem gruf

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

	Ref	Expression
Assertion	gruf	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → 𝐹 ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		simp3	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → 𝐹 : 𝐴 ⟶ 𝑈 )
2	1	feqmptd	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )
3		fvex	⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
4	3	fnasrn	⊢ ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) = ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ )
5	2 4	eqtrdi	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → 𝐹 = ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) )
6		simpl1	⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑈 ∈ Univ )
7		gruel	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑈 )
8	7	3expa	⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑈 )
9	8	3adantl3	⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ 𝑈 )
10		ffvelcdm	⊢ ( ( 𝐹 : 𝐴 ⟶ 𝑈 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑈 )
11	10	3ad2antl3	⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑈 )
12		gruop	⊢ ( ( 𝑈 ∈ Univ ∧ 𝑥 ∈ 𝑈 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑈 ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝑈 )
13	6 9 11 12	syl3anc	⊢ ( ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) ∧ 𝑥 ∈ 𝐴 ) → ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ∈ 𝑈 )
14	13	fmpttd	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) : 𝐴 ⟶ 𝑈 )
15		grurn	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) : 𝐴 ⟶ 𝑈 ) → ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) ∈ 𝑈 )
16	14 15	syld3an3	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → ran ( 𝑥 ∈ 𝐴 ↦ ⟨ 𝑥 , ( 𝐹 ‘ 𝑥 ) ⟩ ) ∈ 𝑈 )
17	5 16	eqeltrd	⊢ ( ( 𝑈 ∈ Univ ∧ 𝐴 ∈ 𝑈 ∧ 𝐹 : 𝐴 ⟶ 𝑈 ) → 𝐹 ∈ 𝑈 )