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	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ Scott 𝐵 ) → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		elscottrankss	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐶 ) )
2	1	3adant3	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ Scott 𝐵 ) → ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐶 ) )
3		scottrankeqel	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ( rank ‘ 𝐶 ) = ( rank ‘ 𝐴 ) ) → 𝐶 ∈ Scott 𝐵 )
4	3	3expia	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( ( rank ‘ 𝐶 ) = ( rank ‘ 𝐴 ) → 𝐶 ∈ Scott 𝐵 ) )
5	4	necon3bd	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ) → ( ¬ 𝐶 ∈ Scott 𝐵 → ( rank ‘ 𝐶 ) ≠ ( rank ‘ 𝐴 ) ) )
6	5	3impia	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ Scott 𝐵 ) → ( rank ‘ 𝐶 ) ≠ ( rank ‘ 𝐴 ) )
7	6	necomd	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ Scott 𝐵 ) → ( rank ‘ 𝐴 ) ≠ ( rank ‘ 𝐶 ) )
8		rankon	⊢ ( rank ‘ 𝐴 ) ∈ On
9		rankon	⊢ ( rank ‘ 𝐶 ) ∈ On
10		onelpss	⊢ ( ( ( rank ‘ 𝐴 ) ∈ On ∧ ( rank ‘ 𝐶 ) ∈ On ) → ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ↔ ( ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐴 ) ≠ ( rank ‘ 𝐶 ) ) ) )
11	8 9 10	mp2an	⊢ ( ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) ↔ ( ( rank ‘ 𝐴 ) ⊆ ( rank ‘ 𝐶 ) ∧ ( rank ‘ 𝐴 ) ≠ ( rank ‘ 𝐶 ) ) )
12	2 7 11	sylanbrc	⊢ ( ( 𝐴 ∈ Scott 𝐵 ∧ 𝐶 ∈ 𝐵 ∧ ¬ 𝐶 ∈ Scott 𝐵 ) → ( rank ‘ 𝐴 ) ∈ ( rank ‘ 𝐶 ) )