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 ω

Proof

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