Theorem elscottrank

Description: The rank of an element in a Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026)

	Ref	Expression
Assertion	elscottrank	⊢ ( 𝐴 ∈ Scott 𝐵 → ( rank ‘ 𝐴 ) = ∩ ( rank “ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		fveqeq2	⊢ ( 𝑥 = 𝐴 → ( ( rank ‘ 𝑥 ) = ∩ ( rank “ 𝐵 ) ↔ ( rank ‘ 𝐴 ) = ∩ ( rank “ 𝐵 ) ) )
2		dfscott2	⊢ Scott 𝐵 = { 𝑥 ∈ 𝐵 ∣ ( rank ‘ 𝑥 ) = ∩ ( rank “ 𝐵 ) }
3	1 2	elrab2	⊢ ( 𝐴 ∈ Scott 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ( rank ‘ 𝐴 ) = ∩ ( rank “ 𝐵 ) ) )
4	3	simprbi	⊢ ( 𝐴 ∈ Scott 𝐵 → ( rank ‘ 𝐴 ) = ∩ ( rank “ 𝐵 ) )