Metamath Proof Explorer

Theorem tron

Description: The class of all ordinal numbers is transitive. (Contributed by NM, 4-May-2009)

Ref Expression
Assertion tron 
|- Tr On

Proof

Step Hyp Ref Expression
1 dftr3 
 |-  ( Tr On <-> A. x e. On x C_ On )
2 vex 
 |-  x e. _V
3 2 elon 
 |-  ( x e. On <-> Ord x )
4 ordelord 
 |-  ( ( Ord x /\ y e. x ) -> Ord y )
5 3 4 sylanb 
 |-  ( ( x e. On /\ y e. x ) -> Ord y )
6 5 ex 
 |-  ( x e. On -> ( y e. x -> Ord y ) )
7 vex 
 |-  y e. _V
8 7 elon 
 |-  ( y e. On <-> Ord y )
9 6 8 imbitrrdi 
 |-  ( x e. On -> ( y e. x -> y e. On ) )
10 9 ssrdv 
 |-  ( x e. On -> x C_ On )
11 1 10 mprgbir 
 |-  Tr On