Theorem grurankrcld

Description: If a Grothendieck universe contains a set's rank, it contains that set. (Contributed by Rohan Ridenour, 9-Aug-2023)

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

Proof

Step	Hyp	Ref	Expression
1		grurankrcld.1	$$⊢\phi \to G\in \mathrm{Univ}$$
2		grurankrcld.2	$$⊢\phi \to \mathrm{rank}\left(A\right)\in G$$
3		grurankrcld.3	$$⊢\phi \to A\in V$$
4	1 2	grur1cld	$$⊢\phi \to R_1\left(\mathrm{rank}\left(A\right)\right)\in G$$
5		r1rankid	$$⊢A\in V\to A\subseteq R_1\left(\mathrm{rank}\left(A\right)\right)$$
6	3 5	syl	$$⊢\phi \to A\subseteq R_1\left(\mathrm{rank}\left(A\right)\right)$$
7		gruss	$$⊢\left(G\in \mathrm{Univ}\wedge R_1\left(\mathrm{rank}\left(A\right)\right)\in G\wedge A\subseteq R_1\left(\mathrm{rank}\left(A\right)\right)\right)\to A\in G$$
8	1 4 6 7	syl3anc	$$⊢\phi \to A\in G$$