![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ordzsl | Structured version Visualization version GIF version |
Description: An ordinal is zero, a successor ordinal, or a limit ordinal. (Contributed by NM, 1-Oct-2003.) |
Ref | Expression |
---|---|
ordzsl | ⊢ (Ord 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orduninsuc 7275 | . . . . . 6 ⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ ¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥)) | |
2 | 1 | biimprd 240 | . . . . 5 ⊢ (Ord 𝐴 → (¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥 → 𝐴 = ∪ 𝐴)) |
3 | unizlim 6055 | . . . . 5 ⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ (𝐴 = ∅ ∨ Lim 𝐴))) | |
4 | 2, 3 | sylibd 231 | . . . 4 ⊢ (Ord 𝐴 → (¬ ∃𝑥 ∈ On 𝐴 = suc 𝑥 → (𝐴 = ∅ ∨ Lim 𝐴))) |
5 | 4 | orrd 890 | . . 3 ⊢ (Ord 𝐴 → (∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 = ∅ ∨ Lim 𝐴))) |
6 | 3orass 1111 | . . . 4 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ (𝐴 = ∅ ∨ (∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴))) | |
7 | or12 945 | . . . 4 ⊢ ((𝐴 = ∅ ∨ (∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴)) ↔ (∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 = ∅ ∨ Lim 𝐴))) | |
8 | 6, 7 | bitri 267 | . . 3 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) ↔ (∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ (𝐴 = ∅ ∨ Lim 𝐴))) |
9 | 5, 8 | sylibr 226 | . 2 ⊢ (Ord 𝐴 → (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴)) |
10 | ord0 5991 | . . . 4 ⊢ Ord ∅ | |
11 | ordeq 5946 | . . . 4 ⊢ (𝐴 = ∅ → (Ord 𝐴 ↔ Ord ∅)) | |
12 | 10, 11 | mpbiri 250 | . . 3 ⊢ (𝐴 = ∅ → Ord 𝐴) |
13 | suceloni 7245 | . . . . . 6 ⊢ (𝑥 ∈ On → suc 𝑥 ∈ On) | |
14 | eleq1 2864 | . . . . . 6 ⊢ (𝐴 = suc 𝑥 → (𝐴 ∈ On ↔ suc 𝑥 ∈ On)) | |
15 | 13, 14 | syl5ibr 238 | . . . . 5 ⊢ (𝐴 = suc 𝑥 → (𝑥 ∈ On → 𝐴 ∈ On)) |
16 | eloni 5949 | . . . . 5 ⊢ (𝐴 ∈ On → Ord 𝐴) | |
17 | 15, 16 | syl6com 37 | . . . 4 ⊢ (𝑥 ∈ On → (𝐴 = suc 𝑥 → Ord 𝐴)) |
18 | 17 | rexlimiv 3206 | . . 3 ⊢ (∃𝑥 ∈ On 𝐴 = suc 𝑥 → Ord 𝐴) |
19 | limord 5998 | . . 3 ⊢ (Lim 𝐴 → Ord 𝐴) | |
20 | 12, 18, 19 | 3jaoi 1553 | . 2 ⊢ ((𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴) → Ord 𝐴) |
21 | 9, 20 | impbii 201 | 1 ⊢ (Ord 𝐴 ↔ (𝐴 = ∅ ∨ ∃𝑥 ∈ On 𝐴 = suc 𝑥 ∨ Lim 𝐴)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 ↔ wb 198 ∨ wo 874 ∨ w3o 1107 = wceq 1653 ∈ wcel 2157 ∃wrex 3088 ∅c0 4113 ∪ cuni 4626 Ord word 5938 Oncon0 5939 Lim wlim 5940 suc csuc 5941 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-sep 4973 ax-nul 4981 ax-pr 5095 ax-un 7181 |
This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-ral 3092 df-rex 3093 df-rab 3096 df-v 3385 df-sbc 3632 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-pss 3783 df-nul 4114 df-if 4276 df-pw 4349 df-sn 4367 df-pr 4369 df-tp 4371 df-op 4373 df-uni 4627 df-br 4842 df-opab 4904 df-tr 4944 df-eprel 5223 df-po 5231 df-so 5232 df-fr 5269 df-we 5271 df-ord 5942 df-on 5943 df-lim 5944 df-suc 5945 |
This theorem is referenced by: onzsl 7278 tfrlem16 7726 omeulem1 7900 oaabs2 7963 rankxplim3 8992 rankxpsuc 8993 cardlim 9082 cardaleph 9196 cflim2 9371 dfrdg2 32205 |
Copyright terms: Public domain | W3C validator |