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\in B\to ScottB\subseteq R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		rankscottu	$$⊢A\in B\to \mathrm{rank}\left(ScottB\right)\subseteq \mathrm{suc}\mathrm{rank}\left(A\right)$$
2		rankon	$$⊢\mathrm{rank}\left(A\right)\in \mathrm{On}$$
3	2	onsuci	$$⊢\mathrm{suc}\mathrm{rank}\left(A\right)\in \mathrm{On}$$
4		scottex	$$⊢ScottB\in \mathrm{V}$$
5	4	rankr1b	$$⊢\mathrm{suc}\mathrm{rank}\left(A\right)\in \mathrm{On}\to \left(ScottB\subseteq R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)\leftrightarrow \mathrm{rank}\left(ScottB\right)\subseteq \mathrm{suc}\mathrm{rank}\left(A\right)\right)$$
6	3 5	ax-mp	$$⊢ScottB\subseteq R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)\leftrightarrow \mathrm{rank}\left(ScottB\right)\subseteq \mathrm{suc}\mathrm{rank}\left(A\right)$$
7	1 6	sylibr	$$⊢A\in B\to ScottB\subseteq R_1\left(\mathrm{suc}\mathrm{rank}\left(A\right)\right)$$