Theorem scottssr1

Description: Relationship between a Scott's trick set and the cumulative hierarchy. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	scottssr1	|- ( A e. B -> Scott B C_ ( R1 ` suc ( rank ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		rankscottu	|- ( A e. B -> ( rank ` Scott B ) C_ suc ( rank ` A ) )
2		rankon	|- ( rank ` A ) e. On
3	2	onsuci	|- suc ( rank ` A ) e. On
4		scottex2	|- Scott B e. _V
5	4	rankr1b	|- ( suc ( rank ` A ) e. On -> ( Scott B C_ ( R1 ` suc ( rank ` A ) ) <-> ( rank ` Scott B ) C_ suc ( rank ` A ) ) )
6	3 5	ax-mp	|- ( Scott B C_ ( R1 ` suc ( rank ` A ) ) <-> ( rank ` Scott B ) C_ suc ( rank ` A ) )
7	1 6	sylibr	|- ( A e. B -> Scott B C_ ( R1 ` suc ( rank ` A ) ) )