Theorem gruscottcld

Description: If a Grothendieck universe contains an element of a Scott's trick set, it contains the Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypotheses	gruscottcld.1	⊢ ( 𝜑 → 𝐺 ∈ Univ )
	gruscottcld.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐺 )
	gruscottcld.3	⊢ ( 𝜑 → 𝐵 ∈ Scott 𝐴 )
Assertion	gruscottcld	⊢ ( 𝜑 → Scott 𝐴 ∈ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		gruscottcld.1	⊢ ( 𝜑 → 𝐺 ∈ Univ )
2		gruscottcld.2	⊢ ( 𝜑 → 𝐵 ∈ 𝐺 )
3		gruscottcld.3	⊢ ( 𝜑 → 𝐵 ∈ Scott 𝐴 )
4	3	scottrankd	⊢ ( 𝜑 → ( rank ‘ Scott 𝐴 ) = suc ( rank ‘ 𝐵 ) )
5	1 2	grurankcld	⊢ ( 𝜑 → ( rank ‘ 𝐵 ) ∈ 𝐺 )
6	1 5	grusucd	⊢ ( 𝜑 → suc ( rank ‘ 𝐵 ) ∈ 𝐺 )
7	4 6	eqeltrd	⊢ ( 𝜑 → ( rank ‘ Scott 𝐴 ) ∈ 𝐺 )
8		scottex	⊢ Scott 𝐴 ∈ V
9	8	a1i	⊢ ( 𝜑 → Scott 𝐴 ∈ V )
10	1 7 9	grurankrcld	⊢ ( 𝜑 → Scott 𝐴 ∈ 𝐺 )