Theorem grurn

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

Proof

Step	Hyp	Ref	Expression
1		simp1	|- ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> U e. Univ )
2		gruurn	|- ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> U. ran F e. U )
3		grupw	|- ( ( U e. Univ /\ U. ran F e. U ) -> ~P U. ran F e. U )
4	1 2 3	syl2anc	|- ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> ~P U. ran F e. U )
5		pwuni	|- ran F C_ ~P U. ran F
6	5	a1i	|- ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> ran F C_ ~P U. ran F )
7		gruss	|- ( ( U e. Univ /\ ~P U. ran F e. U /\ ran F C_ ~P U. ran F ) -> ran F e. U )
8	1 4 6 7	syl3anc	|- ( ( U e. Univ /\ A e. U /\ F : A --> U ) -> ran F e. U )