Theorem elscottrankeq

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

	Ref	Expression
Assertion	elscottrankeq	⊢ ( ( 𝐴 ∈ Scott 𝐶 ∧ 𝐵 ∈ Scott 𝐶 ) → ( rank ‘ 𝐴 ) = ( rank ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝐴 ∈ Scott 𝐶 ∧ 𝐵 ∈ Scott 𝐶 ) → 𝐴 ∈ Scott 𝐶 )
2		simpr	⊢ ( ( 𝐴 ∈ Scott 𝐶 ∧ 𝐵 ∈ Scott 𝐶 ) → 𝐵 ∈ Scott 𝐶 )
3	1 2	scottelrankd	⊢ ( ( 𝐴 ∈ Scott 𝐶 ∧ 𝐵 ∈ Scott 𝐶 ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐵 ) )
4	2 1	scottelrankd	⊢ ( ( 𝐴 ∈ Scott 𝐶 ∧ 𝐵 ∈ Scott 𝐶 ) → ( rank ‘ 𝐵 ) ⊆ ( rank ‘ 𝐴 ) )
5	3 4	eqssd	⊢ ( ( 𝐴 ∈ Scott 𝐶 ∧ 𝐵 ∈ Scott 𝐶 ) → ( rank ‘ 𝐴 ) = ( rank ‘ 𝐵 ) )