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 e. Univ /\ A e. U /\ F : A --> U ) -> F e. U )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> F : A --> U )
2 1 feqmptd 
 |-  ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> F = ( x e. A |-> ( F ` x ) ) )
3 fvex 
 |-  ( F ` x ) e. _V
4 3 fnasrn 
 |-  ( x e. A |-> ( F ` x ) ) = ran ( x e. A |-> <. x , ( F ` x ) >. )
5 2 4 eqtrdi 
 |-  ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> F = ran ( x e. A |-> <. x , ( F ` x ) >. ) )
6 simpl1 
 |-  ( ( ( U e. Univ /\ A e. U /\ F : A --> U ) /\ x e. A ) -> U e. Univ )
7 gruel 
 |-  ( ( U e. Univ /\ A e. U /\ x e. A ) -> x e. U )
8 7 3expa 
 |-  ( ( ( U e. Univ /\ A e. U ) /\ x e. A ) -> x e. U )
9 8 3adantl3 
 |-  ( ( ( U e. Univ /\ A e. U /\ F : A --> U ) /\ x e. A ) -> x e. U )
10 ffvelrn 
 |-  ( ( F : A --> U /\ x e. A ) -> ( F ` x ) e. U )
11 10 3ad2antl3 
 |-  ( ( ( U e. Univ /\ A e. U /\ F : A --> U ) /\ x e. A ) -> ( F ` x ) e. U )
12 gruop 
 |-  ( ( U e. Univ /\ x e. U /\ ( F ` x ) e. U ) -> <. x , ( F ` x ) >. e. U )
13 6 9 11 12 syl3anc 
 |-  ( ( ( U e. Univ /\ A e. U /\ F : A --> U ) /\ x e. A ) -> <. x , ( F ` x ) >. e. U )
14 13 fmpttd 
 |-  ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> ( x e. A |-> <. x , ( F ` x ) >. ) : A --> U )
15 grurn 
 |-  ( ( U e. Univ /\ A e. U /\ ( x e. A |-> <. x , ( F ` x ) >. ) : A --> U ) -> ran ( x e. A |-> <. x , ( F ` x ) >. ) e. U )
16 14 15 syld3an3 
 |-  ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> ran ( x e. A |-> <. x , ( F ` x ) >. ) e. U )
17 5 16 eqeltrd 
 |-  ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> F e. U )