Theorem scottrankeqel

Description: If a member of the input set has the same rank as a member of the Scott's trick set, then it is also a member of the Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026)

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

Proof

Step	Hyp	Ref	Expression
1		elscottrank	|- ( A e. Scott B -> ( rank ` A ) = |^| ( rank " B ) )
2	1	3ad2ant1	|- ( ( A e. Scott B /\ C e. B /\ ( rank ` C ) = ( rank ` A ) ) -> ( rank ` A ) = |^| ( rank " B ) )
3		eqtr	|- ( ( ( rank ` C ) = ( rank ` A ) /\ ( rank ` A ) = |^| ( rank " B ) ) -> ( rank ` C ) = |^| ( rank " B ) )
4	3	3ad2antl3	|- ( ( ( A e. Scott B /\ C e. B /\ ( rank ` C ) = ( rank ` A ) ) /\ ( rank ` A ) = |^| ( rank " B ) ) -> ( rank ` C ) = |^| ( rank " B ) )
5	2 4	mpdan	|- ( ( A e. Scott B /\ C e. B /\ ( rank ` C ) = ( rank ` A ) ) -> ( rank ` C ) = |^| ( rank " B ) )
6		elscott2	|- ( C e. Scott B <-> ( C e. B /\ ( rank ` C ) = |^| ( rank " B ) ) )
7	6	baib	|- ( C e. B -> ( C e. Scott B <-> ( rank ` C ) = |^| ( rank " B ) ) )
8	7	3ad2ant2	|- ( ( A e. Scott B /\ C e. B /\ ( rank ` C ) = ( rank ` A ) ) -> ( C e. Scott B <-> ( rank ` C ) = |^| ( rank " B ) ) )
9	5 8	mpbird	|- ( ( A e. Scott B /\ C e. B /\ ( rank ` C ) = ( rank ` A ) ) -> C e. Scott B )