Theorem gruurn

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

Proof

Step	Hyp	Ref	Expression
1		elmapg	|- ( ( U e. Univ /\ A e. U ) -> ( F e. ( U ^m A ) <-> F : A --> U ) )
2		elgrug	|- ( U e. Univ -> ( U e. Univ <-> ( Tr U /\ A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) ) ) )
3	2	ibi	|- ( U e. Univ -> ( Tr U /\ A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) ) )
4	3	simprd	|- ( U e. Univ -> A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) )
5		rneq	|- ( y = F -> ran y = ran F )
6	5	unieqd	|- ( y = F -> U. ran y = U. ran F )
7	6	eleq1d	|- ( y = F -> ( U. ran y e. U <-> U. ran F e. U ) )
8	7	rspccv	|- ( A. y e. ( U ^m x ) U. ran y e. U -> ( F e. ( U ^m x ) -> U. ran F e. U ) )
9	8	3ad2ant3	|- ( ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) -> ( F e. ( U ^m x ) -> U. ran F e. U ) )
10	9	ralimi	|- ( A. x e. U ( ~P x e. U /\ A. y e. U { x , y } e. U /\ A. y e. ( U ^m x ) U. ran y e. U ) -> A. x e. U ( F e. ( U ^m x ) -> U. ran F e. U ) )
11		oveq2	|- ( x = A -> ( U ^m x ) = ( U ^m A ) )
12	11	eleq2d	|- ( x = A -> ( F e. ( U ^m x ) <-> F e. ( U ^m A ) ) )
13	12	imbi1d	|- ( x = A -> ( ( F e. ( U ^m x ) -> U. ran F e. U ) <-> ( F e. ( U ^m A ) -> U. ran F e. U ) ) )
14	13	rspccv	|- ( A. x e. U ( F e. ( U ^m x ) -> U. ran F e. U ) -> ( A e. U -> ( F e. ( U ^m A ) -> U. ran F e. U ) ) )
15	4 10 14	3syl	|- ( U e. Univ -> ( A e. U -> ( F e. ( U ^m A ) -> U. ran F e. U ) ) )
16	15	imp	|- ( ( U e. Univ /\ A e. U ) -> ( F e. ( U ^m A ) -> U. ran F e. U ) )
17	1 16	sylbird	|- ( ( U e. Univ /\ A e. U ) -> ( F : A --> U -> U. ran F e. U ) )
18	17	3impia	|- ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> U. ran F e. U )