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 ∈ Scott B ∧ C ∈ B ∧ ¬ C ∈ Scott B → rank ⁡ A ∈ rank ⁡ C

Proof

Step Hyp Ref Expression
1 elscottrankss ⊢ A ∈ Scott B ∧ C ∈ B → rank ⁡ A ⊆ rank ⁡ C
2 1 3adant3 ⊢ A ∈ Scott B ∧ C ∈ B ∧ ¬ C ∈ Scott B → rank ⁡ A ⊆ rank ⁡ C
3 scottrankeqel ⊢ A ∈ Scott B ∧ C ∈ B ∧ rank ⁡ C = rank ⁡ A → C ∈ Scott B
4 3 3expia ⊢ A ∈ Scott B ∧ C ∈ B → rank ⁡ C = rank ⁡ A → C ∈ Scott B
5 4 necon3bd ⊢ A ∈ Scott B ∧ C ∈ B → ¬ C ∈ Scott B → rank ⁡ C ≠ rank ⁡ A
6 5 3impia ⊢ A ∈ Scott B ∧ C ∈ B ∧ ¬ C ∈ Scott B → rank ⁡ C ≠ rank ⁡ A
7 6 necomd ⊢ A ∈ Scott B ∧ C ∈ B ∧ ¬ C ∈ Scott B → rank ⁡ A ≠ rank ⁡ C
8 rankon ⊢ rank ⁡ A ∈ On
9 rankon ⊢ rank ⁡ C ∈ On
10 onelpss ⊢ rank ⁡ A ∈ On ∧ rank ⁡ C ∈ On → rank ⁡ A ∈ rank ⁡ C ↔ rank ⁡ A ⊆ rank ⁡ C ∧ rank ⁡ A ≠ rank ⁡ C
11 8 9 10 mp2an ⊢ rank ⁡ A ∈ rank ⁡ C ↔ rank ⁡ A ⊆ rank ⁡ C ∧ rank ⁡ A ≠ rank ⁡ C
12 2 7 11 sylanbrc ⊢ A ∈ Scott B ∧ C ∈ B ∧ ¬ C ∈ Scott B → rank ⁡ A ∈ rank ⁡ C