Description: A set belongs to an ordinal number iff its successor is a subset of the ordinal number. Exercise 8 of TakeutiZaring p. 42 and its converse. (Contributed by NM, 16-Sep-1995)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | onssi.1 | |- A e. On |
|
| onsucssi.2 | |- B e. On |
||
| Assertion | onsucssi | |- ( A e. B <-> suc A C_ B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | onssi.1 | |- A e. On |
|
| 2 | onsucssi.2 | |- B e. On |
|
| 3 | 2 | onordi | |- Ord B |
| 4 | ordelsuc | |- ( ( A e. On /\ Ord B ) -> ( A e. B <-> suc A C_ B ) ) |
|
| 5 | 1 3 4 | mp2an | |- ( A e. B <-> suc A C_ B ) |