Metamath Proof Explorer

Theorem nelscottrankgt

Description: If a member of the input set is not a member of the Scott's trick set, then its rank is greater than the rank of a member of the Scott's trick set. (Contributed by BTernaryTau, 10-Jul-2026)

Ref Expression
Assertion nelscottrankgt 
|- ( ( A e. Scott B /\ C e. B /\ -. C e. Scott B ) -> ( rank ` A ) e. ( rank ` C ) )

Proof

Step Hyp Ref Expression
1 elscottrankss 
 |-  ( ( A e. Scott B /\ C e. B ) -> ( rank ` A ) C_ ( rank ` C ) )
2 1 3adant3 
 |-  ( ( A e. Scott B /\ C e. B /\ -. C e. Scott B ) -> ( rank ` A ) C_ ( rank ` C ) )
3 scottrankeqel 
 |-  ( ( A e. Scott B /\ C e. B /\ ( rank ` C ) = ( rank ` A ) ) -> C e. Scott B )
4 3 3expia 
 |-  ( ( A e. Scott B /\ C e. B ) -> ( ( rank ` C ) = ( rank ` A ) -> C e. Scott B ) )
5 4 necon3bd 
 |-  ( ( A e. Scott B /\ C e. B ) -> ( -. C e. Scott B -> ( rank ` C ) =/= ( rank ` A ) ) )
6 5 3impia 
 |-  ( ( A e. Scott B /\ C e. B /\ -. C e. Scott B ) -> ( rank ` C ) =/= ( rank ` A ) )
7 6 necomd 
 |-  ( ( A e. Scott B /\ C e. B /\ -. C e. Scott B ) -> ( rank ` A ) =/= ( rank ` C ) )
8 rankon 
 |-  ( rank ` A ) e. On
9 rankon 
 |-  ( rank ` C ) e. On
10 onelpss 
 |-  ( ( ( rank ` A ) e. On /\ ( rank ` C ) e. On ) -> ( ( rank ` A ) e. ( rank ` C ) <-> ( ( rank ` A ) C_ ( rank ` C ) /\ ( rank ` A ) =/= ( rank ` C ) ) ) )
11 8 9 10 mp2an 
 |-  ( ( rank ` A ) e. ( rank ` C ) <-> ( ( rank ` A ) C_ ( rank ` C ) /\ ( rank ` A ) =/= ( rank ` C ) ) )
12 2 7 11 sylanbrc 
 |-  ( ( A e. Scott B /\ C e. B /\ -. C e. Scott B ) -> ( rank ` A ) e. ( rank ` C ) )