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	|- ( ph -> G e. Univ )
	grurankrcld.2	|- ( ph -> ( rank ` A ) e. G )
	grurankrcld.3	|- ( ph -> A e. V )
Assertion	grurankrcld	|- ( ph -> A e. G )

Proof

Step	Hyp	Ref	Expression
1		grurankrcld.1	|- ( ph -> G e. Univ )
2		grurankrcld.2	|- ( ph -> ( rank ` A ) e. G )
3		grurankrcld.3	|- ( ph -> A e. V )
4	1 2	grur1cld	|- ( ph -> ( R1 ` ( rank ` A ) ) e. G )
5		r1rankid	|- ( A e. V -> A C_ ( R1 ` ( rank ` A ) ) )
6	3 5	syl	|- ( ph -> A C_ ( R1 ` ( rank ` A ) ) )
7		gruss	|- ( ( G e. Univ /\ ( R1 ` ( rank ` A ) ) e. G /\ A C_ ( R1 ` ( rank ` A ) ) ) -> A e. G )
8	1 4 6 7	syl3anc	|- ( ph -> A e. G )