Theorem rankscott

Description: The rank of a nonempty Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026)

	Ref	Expression
Assertion	rankscott	$$⊢A\ne \varnothing \to \mathrm{rank}\left(ScottA\right)=\mathrm{suc}\bigcap \mathrm{rank}\left[A\right]$$

Proof

Step	Hyp	Ref	Expression
1		scott0b	$$⊢A=\varnothing \leftrightarrow ScottA=\varnothing$$
2	1	necon3bii	$$⊢A\ne \varnothing \leftrightarrow ScottA\ne \varnothing$$
3		n0	$$⊢ScottA\ne \varnothing \leftrightarrow \exists xx\in ScottA$$
4	2 3	sylbb	$$⊢A\ne \varnothing \to \exists xx\in ScottA$$
5		id	$$⊢x\in ScottA\to x\in ScottA$$
6	5	scottrankd	$$⊢x\in ScottA\to \mathrm{rank}\left(ScottA\right)=\mathrm{suc}\mathrm{rank}\left(x\right)$$
7		elscottrank	$$⊢x\in ScottA\to \mathrm{rank}\left(x\right)=\bigcap \mathrm{rank}\left[A\right]$$
8	7	suceqd	$$⊢x\in ScottA\to \mathrm{suc}\mathrm{rank}\left(x\right)=\mathrm{suc}\bigcap \mathrm{rank}\left[A\right]$$
9	6 8	eqtrd	$$⊢x\in ScottA\to \mathrm{rank}\left(ScottA\right)=\mathrm{suc}\bigcap \mathrm{rank}\left[A\right]$$
10	9	exlimiv	$$⊢\exists xx\in ScottA\to \mathrm{rank}\left(ScottA\right)=\mathrm{suc}\bigcap \mathrm{rank}\left[A\right]$$
11	4 10	syl	$$⊢A\ne \varnothing \to \mathrm{rank}\left(ScottA\right)=\mathrm{suc}\bigcap \mathrm{rank}\left[A\right]$$