Theorem elscottrankss

Description: Relationship between the ranks of an element in a Scott's trick set and an element in the input class. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	elscottrankss	$$⊢\left(A\in ScottB\wedge C\in B\right)\to \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(C\right)$$

Proof

Step	Hyp	Ref	Expression
1		elscott	$$⊢A\in ScottB\leftrightarrow \left(A\in B\wedge \forall x\in B\mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(x\right)\right)$$
2	1	simprbi	$$⊢A\in ScottB\to \forall x\in B\mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(x\right)$$
3		fveq2	$$⊢x=C\to \mathrm{rank}\left(x\right)=\mathrm{rank}\left(C\right)$$
4	3	sseq2d	$$⊢x=C\to \left(\mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(x\right)\leftrightarrow \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(C\right)\right)$$
5	4	rspccva	$$⊢\left(\forall x\in B\mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(x\right)\wedge C\in B\right)\to \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(C\right)$$
6	2 5	sylan	$$⊢\left(A\in ScottB\wedge C\in B\right)\to \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(C\right)$$