Theorem scottelrankd

Description: Property of a Scott's trick set. (Contributed by Rohan Ridenour, 11-Aug-2023)

	Ref	Expression
Hypotheses	scottelrankd.1	|- ( ph -> B e. Scott A )
	scottelrankd.2	|- ( ph -> C e. Scott A )
Assertion	scottelrankd	|- ( ph -> ( rank ` B ) C_ ( rank ` C ) )

Proof

Step	Hyp	Ref	Expression
1		scottelrankd.1	|- ( ph -> B e. Scott A )
2		scottelrankd.2	|- ( ph -> C e. Scott A )
3		fveq2	|- ( y = C -> ( rank ` y ) = ( rank ` C ) )
4	3	sseq2d	|- ( y = C -> ( ( rank ` B ) C_ ( rank ` y ) <-> ( rank ` B ) C_ ( rank ` C ) ) )
5		df-scott	|- Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }
6	1 5	eleqtrdi	|- ( ph -> B e. { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } )
7		fveq2	|- ( x = B -> ( rank ` x ) = ( rank ` B ) )
8	7	sseq1d	|- ( x = B -> ( ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` B ) C_ ( rank ` y ) ) )
9	8	ralbidv	|- ( x = B -> ( A. y e. A ( rank ` x ) C_ ( rank ` y ) <-> A. y e. A ( rank ` B ) C_ ( rank ` y ) ) )
10	9	elrab	|- ( B e. { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } <-> ( B e. A /\ A. y e. A ( rank ` B ) C_ ( rank ` y ) ) )
11	6 10	sylib	|- ( ph -> ( B e. A /\ A. y e. A ( rank ` B ) C_ ( rank ` y ) ) )
12	11	simprd	|- ( ph -> A. y e. A ( rank ` B ) C_ ( rank ` y ) )
13	2 5	eleqtrdi	|- ( ph -> C e. { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } )
14		elrabi	|- ( C e. { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } -> C e. A )
15	13 14	syl	|- ( ph -> C e. A )
16	4 12 15	rspcdva	|- ( ph -> ( rank ` B ) C_ ( rank ` C ) )