Description: An ordering law for ordinal numbers. (Contributed by NM, 13-Jun-1994)
Ref | Expression | ||
---|---|---|---|
Hypothesis | on.1 | |- A e. On |
|
Assertion | onssnel2i | |- ( B C_ A -> -. A e. B ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | on.1 | |- A e. On |
|
2 | 1 | onirri | |- -. A e. A |
3 | ssel | |- ( B C_ A -> ( A e. B -> A e. A ) ) |
|
4 | 2 3 | mtoi | |- ( B C_ A -> -. A e. B ) |