Theorem dfscott2

Description: Alternate definition of a Scott's trick set. (Contributed by BTernaryTau, 8-Jul-2026)

	Ref	Expression
Assertion	dfscott2	|- Scott A = { x e. A | ( rank ` x ) = |^| ( rank " A ) }

Proof

Step	Hyp	Ref	Expression
1		df-scott	|- Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }
2		rankfn	|- rank Fn _V
3		ssv	|- A C_ _V
4		fnfvintima	|- ( ( rank Fn _V /\ A C_ _V /\ x e. A ) -> ( ( rank ` x ) = |^| ( rank " A ) <-> A. y e. A ( rank ` x ) C_ ( rank ` y ) ) )
5	2 3 4	mp3an12	|- ( x e. A -> ( ( rank ` x ) = |^| ( rank " A ) <-> A. y e. A ( rank ` x ) C_ ( rank ` y ) ) )
6	5	rabbiia	|- { x e. A | ( rank ` x ) = |^| ( rank " A ) } = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }
7	1 6	eqtr4i	|- Scott A = { x e. A | ( rank ` x ) = |^| ( rank " A ) }