Theorem grurankcld

Description: Grothendieck universes are closed under the rank function. (Contributed by Rohan Ridenour, 9-Aug-2023)

	Ref	Expression
Hypotheses	grurankcld.1	|- ( ph -> G e. Univ )
	grurankcld.2	|- ( ph -> A e. G )
Assertion	grurankcld	|- ( ph -> ( rank ` A ) e. G )

Proof

Step	Hyp	Ref	Expression
1		grurankcld.1	|- ( ph -> G e. Univ )
2		grurankcld.2	|- ( ph -> A e. G )
3	1	elexd	|- ( ph -> G e. _V )
4		unir1	|- U. ( R1 " On ) = _V
5	3 4	eleqtrrdi	|- ( ph -> G e. U. ( R1 " On ) )
6		eqid	|- ( G i^i On ) = ( G i^i On )
7	6	grur1	|- ( ( G e. Univ /\ G e. U. ( R1 " On ) ) -> G = ( R1 ` ( G i^i On ) ) )
8	1 5 7	syl2anc	|- ( ph -> G = ( R1 ` ( G i^i On ) ) )
9	2 8	eleqtrd	|- ( ph -> A e. ( R1 ` ( G i^i On ) ) )
10	9	r1rankcld	|- ( ph -> ( rank ` A ) e. ( R1 ` ( G i^i On ) ) )
11	10 8	eleqtrrd	|- ( ph -> ( rank ` A ) e. G )