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	⊢ ( 𝜑 → 𝐺 ∈ Univ )
	grurankrcld.2	⊢ ( 𝜑 → ( rank ‘ 𝐴 ) ∈ 𝐺 )
	grurankrcld.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
Assertion	grurankrcld	⊢ ( 𝜑 → 𝐴 ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		grurankrcld.1	⊢ ( 𝜑 → 𝐺 ∈ Univ )
2		grurankrcld.2	⊢ ( 𝜑 → ( rank ‘ 𝐴 ) ∈ 𝐺 )
3		grurankrcld.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4	1 2	grur1cld	⊢ ( 𝜑 → ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∈ 𝐺 )
5		r1rankid	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
6	3 5	syl	⊢ ( 𝜑 → 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) )
7		gruss	⊢ ( ( 𝐺 ∈ Univ ∧ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ∈ 𝐺 ∧ 𝐴 ⊆ ( 𝑅1 ‘ ( rank ‘ 𝐴 ) ) ) → 𝐴 ∈ 𝐺 )
8	1 4 6 7	syl3anc	⊢ ( 𝜑 → 𝐴 ∈ 𝐺 )