Theorem elscottrankeq

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

	Ref	Expression
Assertion	elscottrankeq	|- ( ( A e. Scott C /\ B e. Scott C ) -> ( rank ` A ) = ( rank ` B ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	|- ( ( A e. Scott C /\ B e. Scott C ) -> A e. Scott C )
2		simpr	|- ( ( A e. Scott C /\ B e. Scott C ) -> B e. Scott C )
3	1 2	scottelrankd	|- ( ( A e. Scott C /\ B e. Scott C ) -> ( rank ` A ) C_ ( rank ` B ) )
4	2 1	scottelrankd	|- ( ( A e. Scott C /\ B e. Scott C ) -> ( rank ` B ) C_ ( rank ` A ) )
5	3 4	eqssd	|- ( ( A e. Scott C /\ B e. Scott C ) -> ( rank ` A ) = ( rank ` B ) )