Theorem grurankcld

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

	Ref	Expression
Hypotheses	grurankcld.1	⊢ ( 𝜑 → 𝐺 ∈ Univ )
	grurankcld.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐺 )
Assertion	grurankcld	⊢ ( 𝜑 → ( rank ‘ 𝐴 ) ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		grurankcld.1	⊢ ( 𝜑 → 𝐺 ∈ Univ )
2		grurankcld.2	⊢ ( 𝜑 → 𝐴 ∈ 𝐺 )
3	1	elexd	⊢ ( 𝜑 → 𝐺 ∈ V )
4		unir1	⊢ ∪ ( 𝑅1 “ On ) = V
5	3 4	eleqtrrdi	⊢ ( 𝜑 → 𝐺 ∈ ∪ ( 𝑅1 “ On ) )
6		eqid	⊢ ( 𝐺 ∩ On ) = ( 𝐺 ∩ On )
7	6	grur1	⊢ ( ( 𝐺 ∈ Univ ∧ 𝐺 ∈ ∪ ( 𝑅1 “ On ) ) → 𝐺 = ( 𝑅1 ‘ ( 𝐺 ∩ On ) ) )
8	1 5 7	syl2anc	⊢ ( 𝜑 → 𝐺 = ( 𝑅1 ‘ ( 𝐺 ∩ On ) ) )
9	2 8	eleqtrd	⊢ ( 𝜑 → 𝐴 ∈ ( 𝑅1 ‘ ( 𝐺 ∩ On ) ) )
10	9	r1rankcld	⊢ ( 𝜑 → ( rank ‘ 𝐴 ) ∈ ( 𝑅1 ‘ ( 𝐺 ∩ On ) ) )
11	10 8	eleqtrrd	⊢ ( 𝜑 → ( rank ‘ 𝐴 ) ∈ 𝐺 )