Theorem ordom 7224

Description: Omega is ordinal. Theorem 7.32 of [TakeutiZaring] p. 43. (Contributed by NM, 18-Oct-1995.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
ordom	⊢ Ord ω

Proof of Theorem ordom

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dftr2 4889	. . 3 ⊢ (Tr ω ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ω) → 𝑦 ∈ ω))
2		onelon 5890	. . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On)
3	2	expcom 398	. . . . . . 7 ⊢ (𝑦 ∈ 𝑥 → (𝑥 ∈ On → 𝑦 ∈ On))
4		limord 5926	. . . . . . . . . . . 12 ⊢ (Lim 𝑧 → Ord 𝑧)
5		ordtr 5879	. . . . . . . . . . . 12 ⊢ (Ord 𝑧 → Tr 𝑧)
6		trel 4894	. . . . . . . . . . . 12 ⊢ (Tr 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑧))
7	4, 5, 6	3syl 18	. . . . . . . . . . 11 ⊢ (Lim 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑧))
8	7	expd 400	. . . . . . . . . 10 ⊢ (Lim 𝑧 → (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)))
9	8	com12 32	. . . . . . . . 9 ⊢ (𝑦 ∈ 𝑥 → (Lim 𝑧 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)))
10	9	a2d 29	. . . . . . . 8 ⊢ (𝑦 ∈ 𝑥 → ((Lim 𝑧 → 𝑥 ∈ 𝑧) → (Lim 𝑧 → 𝑦 ∈ 𝑧)))
11	10	alimdv 1997	. . . . . . 7 ⊢ (𝑦 ∈ 𝑥 → (∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧) → ∀𝑧(Lim 𝑧 → 𝑦 ∈ 𝑧)))
12	3, 11	anim12d 596	. . . . . 6 ⊢ (𝑦 ∈ 𝑥 → ((𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧)) → (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧 → 𝑦 ∈ 𝑧))))
13		elom 7218	. . . . . 6 ⊢ (𝑥 ∈ ω ↔ (𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧)))
14		elom 7218	. . . . . 6 ⊢ (𝑦 ∈ ω ↔ (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧 → 𝑦 ∈ 𝑧)))
15	12, 13, 14	3imtr4g 285	. . . . 5 ⊢ (𝑦 ∈ 𝑥 → (𝑥 ∈ ω → 𝑦 ∈ ω))
16	15	imp 393	. . . 4 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ω) → 𝑦 ∈ ω)
17	16	ax-gen 1870	. . 3 ⊢ ∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ω) → 𝑦 ∈ ω)
18	1, 17	mpgbir 1874	. 2 ⊢ Tr ω
19		omsson 7219	. 2 ⊢ ω ⊆ On
20		ordon 7132	. 2 ⊢ Ord On
21		trssord 5882	. 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω)
22	18, 19, 20, 21	mp3an 1572	1 ⊢ Ord ω

Syntax hints:   → wi 4   ∧ wa 382  ∀wal 1629   ∈ wcel 2145   ⊆ wss 3723  Tr wtr 4887  Ord word 5864  Oncon0 5865  Lim wlim 5866  ωcom 7215

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916  ax-nul 4924  ax-pr 5035  ax-un 7099

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3353  df-sbc 3588  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-br 4788  df-opab 4848  df-tr 4888  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-we 5211  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-om 7216

This theorem is referenced by:  elnn  7225  omon  7226  limom  7230  ssnlim  7233  omsinds  7234  peano5  7239  nnarcl  7853  nnawordex  7874  oaabslem  7880  oaabs2  7882  omabslem  7883  onomeneq  8309  ominf  8331  findcard3  8362  nnsdomg  8378  dffi3  8496  wofib  8609  alephgeom  9108  iscard3  9119  iunfictbso  9140  unctb  9232  ackbij2lem1  9246  ackbij1lem3  9249  ackbij1lem18  9264  ackbij2  9270  cflim2  9290  fin23lem26  9352  fin23lem23  9353  fin23lem27  9355  fin67  9422  alephexp1  9606  pwfseqlem3  9687  pwcdandom  9694  winainflem  9720  wunex2  9765  om2uzoi  12961  ltweuz  12967  fz1isolem  13446  1stcrestlem  21475  hfuni  32627  hfninf  32629  finxpreclem4  33567