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 ω ↔ ∀ 𝑦 ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ω ) → 𝑦 ∈ ω ) )
2		onelon	⊢ ( ( 𝑥 ∈ On ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ On )
3	2	expcom	⊢ ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ On → 𝑦 ∈ On ) )
4		limord	⊢ ( Lim 𝑧 → Ord 𝑧 )
5		ordtr	⊢ ( Ord 𝑧 → Tr 𝑧 )
6		trel	⊢ ( Tr 𝑧 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑧 ) )
7	4 5 6	3syl	⊢ ( Lim 𝑧 → ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧 ) → 𝑦 ∈ 𝑧 ) )
8	7	expd	⊢ ( Lim 𝑧 → ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ) )
9	8	com12	⊢ ( 𝑦 ∈ 𝑥 → ( Lim 𝑧 → ( 𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧 ) ) )
10	9	a2d	⊢ ( 𝑦 ∈ 𝑥 → ( ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) → ( Lim 𝑧 → 𝑦 ∈ 𝑧 ) ) )
11	10	alimdv	⊢ ( 𝑦 ∈ 𝑥 → ( ∀ 𝑧 ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) → ∀ 𝑧 ( Lim 𝑧 → 𝑦 ∈ 𝑧 ) ) )
12	3 11	anim12d	⊢ ( 𝑦 ∈ 𝑥 → ( ( 𝑥 ∈ On ∧ ∀ 𝑧 ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ) → ( 𝑦 ∈ On ∧ ∀ 𝑧 ( Lim 𝑧 → 𝑦 ∈ 𝑧 ) ) ) )
13		elom	⊢ ( 𝑥 ∈ ω ↔ ( 𝑥 ∈ On ∧ ∀ 𝑧 ( Lim 𝑧 → 𝑥 ∈ 𝑧 ) ) )
14		elom	⊢ ( 𝑦 ∈ ω ↔ ( 𝑦 ∈ On ∧ ∀ 𝑧 ( Lim 𝑧 → 𝑦 ∈ 𝑧 ) ) )
15	12 13 14	3imtr4g	⊢ ( 𝑦 ∈ 𝑥 → ( 𝑥 ∈ ω → 𝑦 ∈ ω ) )
16	15	imp	⊢ ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ω ) → 𝑦 ∈ ω )
17	16	ax-gen	⊢ ∀ 𝑥 ( ( 𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ω ) → 𝑦 ∈ ω )
18	1 17	mpgbir	⊢ Tr ω