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	|- ( ph -> G e. Univ )
	gruscottcld.2	|- ( ph -> B e. G )
	gruscottcld.3	|- ( ph -> B e. Scott A )
Assertion	gruscottcld	|- ( ph -> Scott A e. G )

Proof

Step	Hyp	Ref	Expression
1		gruscottcld.1	|- ( ph -> G e. Univ )
2		gruscottcld.2	|- ( ph -> B e. G )
3		gruscottcld.3	|- ( ph -> B e. Scott A )
4	3	scottrankd	|- ( ph -> ( rank ` Scott A ) = suc ( rank ` B ) )
5	1 2	grurankcld	|- ( ph -> ( rank ` B ) e. G )
6	1 5	grusucd	|- ( ph -> suc ( rank ` B ) e. G )
7	4 6	eqeltrd	|- ( ph -> ( rank ` Scott A ) e. G )
8		scottex2	|- Scott A e. _V
9	8	a1i	|- ( ph -> Scott A e. _V )
10	1 7 9	grurankrcld	|- ( ph -> Scott A e. G )