Theorem elscottrankss

Description: Relationship between the ranks of an element in a Scott's trick set and an element in the input set. (Contributed by BTernaryTau, 3-Jul-2026)

	Ref	Expression
Assertion	elscottrankss	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elscott	⊢ ( 𝐴 ∈ Scott 𝐵 ↔ ( 𝐴 ∈ 𝐵 ∧ ∀ 𝑥 ∈ 𝐵 ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) ) )
2	1	simprbi	⊢ ( 𝐴 ∈ Scott 𝐵 → ∀ 𝑥 ∈ 𝐵 ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) )
3		fveq2	⊢ ( 𝑥 = 𝐶 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝐶 ) )
4	3	sseq2d	⊢ ( 𝑥 = 𝐶 → ( ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) ↔ ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐶 ) ) )
5	4	rspccva	⊢ ( ( ∀ 𝑥 ∈ 𝐵 ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝑥 ) ∧ 𝐶 ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐶 ) )
6	2 5	sylan	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐶 ) )