Description: Transitive law for ordinal numbers. Theorem 7M(b) of Enderton p. 192. Theorem 1.9(ii) of Schloeder p. 1. (Contributed by NM, 11-Aug-1994)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | ontr1 | |- ( C e. On -> ( ( A e. B /\ B e. C ) -> A e. C ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | eloni | |- ( C e. On -> Ord C ) |
|
| 2 | ordtr1 | |- ( Ord C -> ( ( A e. B /\ B e. C ) -> A e. C ) ) |
|
| 3 | 1 2 | syl | |- ( C e. On -> ( ( A e. B /\ B e. C ) -> A e. C ) ) |