Theorem grurankcld

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

	Ref	Expression
Hypotheses	grurankcld.1	$$⊢\phi \to G\in \mathrm{Univ}$$
	grurankcld.2	$$⊢\phi \to A\in G$$
Assertion	grurankcld	$$⊢\phi \to \mathrm{rank}\left(A\right)\in G$$

Proof

Step	Hyp	Ref	Expression
1		grurankcld.1	$$⊢\phi \to G\in \mathrm{Univ}$$
2		grurankcld.2	$$⊢\phi \to A\in G$$
3	1	elexd	$$⊢\phi \to G\in \mathrm{V}$$
4		unir1	$$⊢\bigcup R_1\left[\mathrm{On}\right]=\mathrm{V}$$
5	3 4	eleqtrrdi	$$⊢\phi \to G\in \bigcup R_1\left[\mathrm{On}\right]$$
6		eqid	$$⊢G\cap \mathrm{On}=G\cap \mathrm{On}$$
7	6	grur1	$$⊢\left(G\in \mathrm{Univ}\wedge G\in \bigcup R_1\left[\mathrm{On}\right]\right)\to G=R_1\left(G\cap \mathrm{On}\right)$$
8	1 5 7	syl2anc	$$⊢\phi \to G=R_1\left(G\cap \mathrm{On}\right)$$
9	2 8	eleqtrd	$$⊢\phi \to A\in R_1\left(G\cap \mathrm{On}\right)$$
10	9	r1rankcld	$$⊢\phi \to \mathrm{rank}\left(A\right)\in R_1\left(G\cap \mathrm{On}\right)$$
11	10 8	eleqtrrd	$$⊢\phi \to \mathrm{rank}\left(A\right)\in G$$