Metamath Proof Explorer

Theorem scottrankd

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

Ref Expression
Hypothesis scottrankd.1 
|- ( ph -> B e. Scott A )
Assertion scottrankd 
|- ( ph -> ( rank ` Scott A ) = suc ( rank ` B ) )

Proof

Step Hyp Ref Expression
1 scottrankd.1 
 |-  ( ph -> B e. Scott A )
2 scottex2 
 |-  Scott A e. _V
3 2 rankval4 
 |-  ( rank ` Scott A ) = U_ x e. Scott A suc ( rank ` x )
4 3 a1i 
 |-  ( ph -> ( rank ` Scott A ) = U_ x e. Scott A suc ( rank ` x ) )
5 1 adantr 
 |-  ( ( ph /\ x e. Scott A ) -> B e. Scott A )
6 simpr 
 |-  ( ( ph /\ x e. Scott A ) -> x e. Scott A )
7 5 6 scottelrankd 
 |-  ( ( ph /\ x e. Scott A ) -> ( rank ` B ) C_ ( rank ` x ) )
8 6 5 scottelrankd 
 |-  ( ( ph /\ x e. Scott A ) -> ( rank ` x ) C_ ( rank ` B ) )
9 7 8 eqssd 
 |-  ( ( ph /\ x e. Scott A ) -> ( rank ` B ) = ( rank ` x ) )
10 9 suceqd 
 |-  ( ( ph /\ x e. Scott A ) -> suc ( rank ` B ) = suc ( rank ` x ) )
11 10 iuneq2dv 
 |-  ( ph -> U_ x e. Scott A suc ( rank ` B ) = U_ x e. Scott A suc ( rank ` x ) )
12 1 ne0d 
 |-  ( ph -> Scott A =/= (/) )
13 iunconst 
 |-  ( Scott A =/= (/) -> U_ x e. Scott A suc ( rank ` B ) = suc ( rank ` B ) )
14 12 13 syl 
 |-  ( ph -> U_ x e. Scott A suc ( rank ` B ) = suc ( rank ` B ) )
15 4 11 14 3eqtr2d 
 |-  ( ph -> ( rank ` Scott A ) = suc ( rank ` B ) )