Metamath Proof Explorer

Theorem rankscott

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

Ref Expression
Assertion rankscott 
|- ( A =/= (/) -> ( rank ` Scott A ) = suc |^| ( rank " A ) )

Proof

Step Hyp Ref Expression
1 scott0b 
 |-  ( A = (/) <-> Scott A = (/) )
2 1 necon3bii 
 |-  ( A =/= (/) <-> Scott A =/= (/) )
3 n0 
 |-  ( Scott A =/= (/) <-> E. x x e. Scott A )
4 2 3 sylbb 
 |-  ( A =/= (/) -> E. x x e. Scott A )
5 id 
 |-  ( x e. Scott A -> x e. Scott A )
6 5 scottrankd 
 |-  ( x e. Scott A -> ( rank ` Scott A ) = suc ( rank ` x ) )
7 elscottrank 
 |-  ( x e. Scott A -> ( rank ` x ) = |^| ( rank " A ) )
8 7 suceqd 
 |-  ( x e. Scott A -> suc ( rank ` x ) = suc |^| ( rank " A ) )
9 6 8 eqtrd 
 |-  ( x e. Scott A -> ( rank ` Scott A ) = suc |^| ( rank " A ) )
10 9 exlimiv 
 |-  ( E. x x e. Scott A -> ( rank ` Scott A ) = suc |^| ( rank " A ) )
11 4 10 syl 
 |-  ( A =/= (/) -> ( rank ` Scott A ) = suc |^| ( rank " A ) )