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 ⁡ ω

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 ⁡ ω