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	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ( rank ‘ 𝐶 ) = ( rank ‘ 𝐴 ) ) → 𝐶 ∈ Scott 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		elscottrank	⊢ ( 𝐴 ∈ Scott 𝐵 → ( rank ‘ 𝐴 ) = ∩ ( rank “ 𝐵 ) )
2	1	3ad2ant1	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ( rank ‘ 𝐶 ) = ( rank ‘ 𝐴 ) ) → ( rank ‘ 𝐴 ) = ∩ ( rank “ 𝐵 ) )
3		eqtr	⊢ ( ( ( rank ‘ 𝐶 ) = ( rank ‘ 𝐴 ) ∧ ( rank ‘ 𝐴 ) = ∩ ( rank “ 𝐵 ) ) → ( rank ‘ 𝐶 ) = ∩ ( rank “ 𝐵 ) )
4	3	3ad2antl3	⊢ ( ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ( rank ‘ 𝐶 ) = ( rank ‘ 𝐴 ) ) ∧ ( rank ‘ 𝐴 ) = ∩ ( rank “ 𝐵 ) ) → ( rank ‘ 𝐶 ) = ∩ ( rank “ 𝐵 ) )
5	2 4	mpdan	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ( rank ‘ 𝐶 ) = ( rank ‘ 𝐴 ) ) → ( rank ‘ 𝐶 ) = ∩ ( rank “ 𝐵 ) )
6		elscott2	⊢ ( 𝐶 ∈ Scott 𝐵 ↔ ( 𝐶 ∈ 𝐵 ∧ ( rank ‘ 𝐶 ) = ∩ ( rank “ 𝐵 ) ) )
7	6	baib	⊢ ( 𝐶 ∈ 𝐵 → ( 𝐶 ∈ Scott 𝐵 ↔ ( rank ‘ 𝐶 ) = ∩ ( rank “ 𝐵 ) ) )
8	7	3ad2ant2	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ( rank ‘ 𝐶 ) = ( rank ‘ 𝐴 ) ) → ( 𝐶 ∈ Scott 𝐵 ↔ ( rank ‘ 𝐶 ) = ∩ ( rank “ 𝐵 ) ) )
9	5 8	mpbird	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ( rank ‘ 𝐶 ) = ( rank ‘ 𝐴 ) ) → 𝐶 ∈ Scott 𝐵 )