Theorem elscottrankeq

Description: Elements in a Scott's trick set have the same rank. (Contributed by BTernaryTau, 9-Jul-2026)

	Ref	Expression
Assertion	elscottrankeq	$$⊢\left(A\in ScottC\wedge B\in ScottC\right)\to \mathrm{rank}\left(A\right)=\mathrm{rank}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpl	$$⊢\left(A\in ScottC\wedge B\in ScottC\right)\to A\in ScottC$$
2		simpr	$$⊢\left(A\in ScottC\wedge B\in ScottC\right)\to B\in ScottC$$
3	1 2	scottelrankd	$$⊢\left(A\in ScottC\wedge B\in ScottC\right)\to \mathrm{rank}\left(A\right)\subseteq \mathrm{rank}\left(B\right)$$
4	2 1	scottelrankd	$$⊢\left(A\in ScottC\wedge B\in ScottC\right)\to \mathrm{rank}\left(B\right)\subseteq \mathrm{rank}\left(A\right)$$
5	3 4	eqssd	$$⊢\left(A\in ScottC\wedge B\in ScottC\right)\to \mathrm{rank}\left(A\right)=\mathrm{rank}\left(B\right)$$