This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem trom

Description: The class of finite ordinals _om is a transitive class. (Contributed by NM, 18-Oct-1995) (Proof shortened by Andrew Salmon, 27-Aug-2011)

Ref Expression
Assertion trom 
|- Tr _om

Proof

Step Hyp Ref Expression
1 dftr2 
 |-  ( Tr _om <-> A. y A. x ( ( y e. x /\ x e. _om ) -> y e. _om ) )
2 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
3 2 expcom 
 |-  ( y e. x -> ( x e. On -> y e. On ) )
4 limord 
 |-  ( Lim z -> Ord z )
5 ordtr 
 |-  ( Ord z -> Tr z )
6 trel 
 |-  ( Tr z -> ( ( y e. x /\ x e. z ) -> y e. z ) )
7 4 5 6 3syl 
 |-  ( Lim z -> ( ( y e. x /\ x e. z ) -> y e. z ) )
8 7 expd 
 |-  ( Lim z -> ( y e. x -> ( x e. z -> y e. z ) ) )
9 8 com12 
 |-  ( y e. x -> ( Lim z -> ( x e. z -> y e. z ) ) )
10 9 a2d 
 |-  ( y e. x -> ( ( Lim z -> x e. z ) -> ( Lim z -> y e. z ) ) )
11 10 alimdv 
 |-  ( y e. x -> ( A. z ( Lim z -> x e. z ) -> A. z ( Lim z -> y e. z ) ) )
12 3 11 anim12d 
 |-  ( y e. x -> ( ( x e. On /\ A. z ( Lim z -> x e. z ) ) -> ( y e. On /\ A. z ( Lim z -> y e. z ) ) ) )
13 elom 
 |-  ( x e. _om <-> ( x e. On /\ A. z ( Lim z -> x e. z ) ) )
14 elom 
 |-  ( y e. _om <-> ( y e. On /\ A. z ( Lim z -> y e. z ) ) )
15 12 13 14 3imtr4g 
 |-  ( y e. x -> ( x e. _om -> y e. _om ) )
16 15 imp 
 |-  ( ( y e. x /\ x e. _om ) -> y e. _om )
17 16 ax-gen 
 |-  A. x ( ( y e. x /\ x e. _om ) -> y e. _om )
18 1 17 mpgbir 
 |-  Tr _om