Metamath Proof Explorer

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 
|- ( ( A e. Scott B /\ C e. B ) -> ( rank ` A ) C_ ( rank ` C ) )

Proof

Step Hyp Ref Expression
1 elscott 
 |-  ( A e. Scott B <-> ( A e. B /\ A. x e. B ( rank ` A ) C_ ( rank ` x ) ) )
2 1 simprbi 
 |-  ( A e. Scott B -> A. x e. B ( rank ` A ) C_ ( rank ` x ) )
3 fveq2 
 |-  ( x = C -> ( rank ` x ) = ( rank ` C ) )
4 3 sseq2d 
 |-  ( x = C -> ( ( rank ` A ) C_ ( rank ` x ) <-> ( rank ` A ) C_ ( rank ` C ) ) )
5 4 rspccva 
 |-  ( ( A. x e. B ( rank ` A ) C_ ( rank ` x ) /\ C e. B ) -> ( rank ` A ) C_ ( rank ` C ) )
6 2 5 sylan 
 |-  ( ( A e. Scott B /\ C e. B ) -> ( rank ` A ) C_ ( rank ` C ) )