Metamath Proof Explorer


Theorem gruf

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

Ref Expression
Assertion gruf U Univ A U F : A U F U

Proof

Step Hyp Ref Expression
1 simp3 U Univ A U F : A U F : A U
2 1 feqmptd U Univ A U F : A U F = x A F x
3 fvex F x V
4 3 fnasrn x A F x = ran x A x F x
5 2 4 eqtrdi U Univ A U F : A U F = ran x A x F x
6 simpl1 U Univ A U F : A U x A U Univ
7 gruel U Univ A U x A x U
8 7 3expa U Univ A U x A x U
9 8 3adantl3 U Univ A U F : A U x A x U
10 ffvelrn F : A U x A F x U
11 10 3ad2antl3 U Univ A U F : A U x A F x U
12 gruop U Univ x U F x U x F x U
13 6 9 11 12 syl3anc U Univ A U F : A U x A x F x U
14 13 fmpttd U Univ A U F : A U x A x F x : A U
15 grurn U Univ A U x A x F x : A U ran x A x F x U
16 14 15 syld3an3 U Univ A U F : A U ran x A x F x U
17 5 16 eqeltrd U Univ A U F : A U F U