![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ordom | Structured version Visualization version GIF version |
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.) |
Ref | Expression |
---|---|
ordom | ⊢ Ord ω |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dftr2 5032 | . . 3 ⊢ (Tr ω ↔ ∀𝑦∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ω) → 𝑦 ∈ ω)) | |
2 | onelon 6054 | . . . . . . . 8 ⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) | |
3 | 2 | expcom 406 | . . . . . . 7 ⊢ (𝑦 ∈ 𝑥 → (𝑥 ∈ On → 𝑦 ∈ On)) |
4 | limord 6088 | . . . . . . . . . . . 12 ⊢ (Lim 𝑧 → Ord 𝑧) | |
5 | ordtr 6043 | . . . . . . . . . . . 12 ⊢ (Ord 𝑧 → Tr 𝑧) | |
6 | trel 5037 | . . . . . . . . . . . 12 ⊢ (Tr 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑧)) | |
7 | 4, 5, 6 | 3syl 18 | . . . . . . . . . . 11 ⊢ (Lim 𝑧 → ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ 𝑧) → 𝑦 ∈ 𝑧)) |
8 | 7 | expd 408 | . . . . . . . . . 10 ⊢ (Lim 𝑧 → (𝑦 ∈ 𝑥 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))) |
9 | 8 | com12 32 | . . . . . . . . 9 ⊢ (𝑦 ∈ 𝑥 → (Lim 𝑧 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧))) |
10 | 9 | a2d 29 | . . . . . . . 8 ⊢ (𝑦 ∈ 𝑥 → ((Lim 𝑧 → 𝑥 ∈ 𝑧) → (Lim 𝑧 → 𝑦 ∈ 𝑧))) |
11 | 10 | alimdv 1875 | . . . . . . 7 ⊢ (𝑦 ∈ 𝑥 → (∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧) → ∀𝑧(Lim 𝑧 → 𝑦 ∈ 𝑧))) |
12 | 3, 11 | anim12d 599 | . . . . . 6 ⊢ (𝑦 ∈ 𝑥 → ((𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧)) → (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧 → 𝑦 ∈ 𝑧)))) |
13 | elom 7399 | . . . . . 6 ⊢ (𝑥 ∈ ω ↔ (𝑥 ∈ On ∧ ∀𝑧(Lim 𝑧 → 𝑥 ∈ 𝑧))) | |
14 | elom 7399 | . . . . . 6 ⊢ (𝑦 ∈ ω ↔ (𝑦 ∈ On ∧ ∀𝑧(Lim 𝑧 → 𝑦 ∈ 𝑧))) | |
15 | 12, 13, 14 | 3imtr4g 288 | . . . . 5 ⊢ (𝑦 ∈ 𝑥 → (𝑥 ∈ ω → 𝑦 ∈ ω)) |
16 | 15 | imp 398 | . . . 4 ⊢ ((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ω) → 𝑦 ∈ ω) |
17 | 16 | ax-gen 1758 | . . 3 ⊢ ∀𝑥((𝑦 ∈ 𝑥 ∧ 𝑥 ∈ ω) → 𝑦 ∈ ω) |
18 | 1, 17 | mpgbir 1762 | . 2 ⊢ Tr ω |
19 | omsson 7400 | . 2 ⊢ ω ⊆ On | |
20 | ordon 7314 | . 2 ⊢ Ord On | |
21 | trssord 6046 | . 2 ⊢ ((Tr ω ∧ ω ⊆ On ∧ Ord On) → Ord ω) | |
22 | 18, 19, 20, 21 | mp3an 1440 | 1 ⊢ Ord ω |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 387 ∀wal 1505 ∈ wcel 2050 ⊆ wss 3829 Tr wtr 5030 Ord word 6028 Oncon0 6029 Lim wlim 6030 ωcom 7396 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2750 ax-sep 5060 ax-nul 5067 ax-pr 5186 ax-un 7279 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2759 df-cleq 2771 df-clel 2846 df-nfc 2918 df-ne 2968 df-ral 3093 df-rex 3094 df-rab 3097 df-v 3417 df-sbc 3682 df-dif 3832 df-un 3834 df-in 3836 df-ss 3843 df-pss 3845 df-nul 4179 df-if 4351 df-sn 4442 df-pr 4444 df-tp 4446 df-op 4448 df-uni 4713 df-br 4930 df-opab 4992 df-tr 5031 df-eprel 5317 df-po 5326 df-so 5327 df-fr 5366 df-we 5368 df-ord 6032 df-on 6033 df-lim 6034 df-suc 6035 df-om 7397 |
This theorem is referenced by: elnn 7406 omon 7407 limom 7411 ssnlim 7414 omsinds 7415 peano5 7420 omsucelsucb 7897 nnarcl 8043 nnawordex 8064 oaabslem 8070 oaabs2 8072 omabslem 8073 onomeneq 8503 ominf 8525 findcard3 8556 nnsdomg 8572 dffi3 8690 wofib 8804 alephgeom 9302 iscard3 9313 iunfictbso 9334 unctb 9425 ackbij2lem1 9439 ackbij1lem3 9442 ackbij1lem18 9457 ackbij2 9463 cflim2 9483 fin23lem26 9545 fin23lem23 9546 fin23lem27 9548 fin67 9615 alephexp1 9799 pwfseqlem3 9880 pwdjundom 9887 winainflem 9913 wunex2 9958 om2uzoi 13138 ltweuz 13144 fz1isolem 13632 1stcrestlem 21764 hfuni 33172 hfninf 33174 finxpreclem4 34122 |
Copyright terms: Public domain | W3C validator |