Description: If one ordinal is less than another, then the successor of the first is less than or equal to the second. Lemma 1.13 of Schloeder p. 2. See ordsucss . (Contributed by RP, 16-Jan-2025)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | onsucss | |- ( A e. On -> ( B e. A -> suc B C_ A ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eloni | |- ( A e. On -> Ord A ) |
|
| 2 | ordsucss | |- ( Ord A -> ( B e. A -> suc B C_ A ) ) |
|
| 3 | 1 2 | syl | |- ( A e. On -> ( B e. A -> suc B C_ A ) ) |