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	$$⊢\phi \to G\in \mathrm{Univ}$$
	gruscottcld.2	$$⊢\phi \to B\in G$$
	gruscottcld.3	$$⊢\phi \to B\in ScottA$$
Assertion	gruscottcld	$$⊢\phi \to ScottA\in G$$

Proof

Step	Hyp	Ref	Expression
1		gruscottcld.1	$$⊢\phi \to G\in \mathrm{Univ}$$
2		gruscottcld.2	$$⊢\phi \to B\in G$$
3		gruscottcld.3	$$⊢\phi \to B\in ScottA$$
4	3	scottrankd	$$⊢\phi \to \mathrm{rank}\left(ScottA\right)=\mathrm{suc}\mathrm{rank}\left(B\right)$$
5	1 2	grurankcld	$$⊢\phi \to \mathrm{rank}\left(B\right)\in G$$
6	1 5	grusucd	$$⊢\phi \to \mathrm{suc}\mathrm{rank}\left(B\right)\in G$$
7	4 6	eqeltrd	$$⊢\phi \to \mathrm{rank}\left(ScottA\right)\in G$$
8		scottex	$$⊢ScottA\in \mathrm{V}$$
9	8	a1i	$$⊢\phi \to ScottA\in \mathrm{V}$$
10	1 7 9	grurankrcld	$$⊢\phi \to ScottA\in G$$