Metamath Proof Explorer

Theorem ontrci

Description: An ordinal number is a transitive class. (Contributed by NM, 11-Jun-1994)

Ref Expression
Hypothesis on.1 
|- A e. On
Assertion ontrci 
|- Tr A

Proof

Step Hyp Ref Expression
1 on.1 
 |-  A e. On
2 1 onordi 
 |-  Ord A
3 ordtr 
 |-  ( Ord A -> Tr A )
4 2 3 ax-mp 
 |-  Tr A