![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > unizlim | Structured version Visualization version GIF version |
Description: An ordinal equal to its own union is either zero or a limit ordinal. (Contributed by NM, 1-Oct-2003.) |
Ref | Expression |
---|---|
unizlim | ⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ (𝐴 = ∅ ∨ Lim 𝐴))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-ne 2970 | . . . . . . 7 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅) | |
2 | df-lim 5981 | . . . . . . . . 9 ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) | |
3 | 2 | biimpri 220 | . . . . . . . 8 ⊢ ((Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) → Lim 𝐴) |
4 | 3 | 3exp 1109 | . . . . . . 7 ⊢ (Ord 𝐴 → (𝐴 ≠ ∅ → (𝐴 = ∪ 𝐴 → Lim 𝐴))) |
5 | 1, 4 | syl5bir 235 | . . . . . 6 ⊢ (Ord 𝐴 → (¬ 𝐴 = ∅ → (𝐴 = ∪ 𝐴 → Lim 𝐴))) |
6 | 5 | com23 86 | . . . . 5 ⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 → (¬ 𝐴 = ∅ → Lim 𝐴))) |
7 | 6 | imp 397 | . . . 4 ⊢ ((Ord 𝐴 ∧ 𝐴 = ∪ 𝐴) → (¬ 𝐴 = ∅ → Lim 𝐴)) |
8 | 7 | orrd 852 | . . 3 ⊢ ((Ord 𝐴 ∧ 𝐴 = ∪ 𝐴) → (𝐴 = ∅ ∨ Lim 𝐴)) |
9 | 8 | ex 403 | . 2 ⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 → (𝐴 = ∅ ∨ Lim 𝐴))) |
10 | uni0 4700 | . . . . 5 ⊢ ∪ ∅ = ∅ | |
11 | 10 | eqcomi 2787 | . . . 4 ⊢ ∅ = ∪ ∅ |
12 | id 22 | . . . 4 ⊢ (𝐴 = ∅ → 𝐴 = ∅) | |
13 | unieq 4679 | . . . 4 ⊢ (𝐴 = ∅ → ∪ 𝐴 = ∪ ∅) | |
14 | 11, 12, 13 | 3eqtr4a 2840 | . . 3 ⊢ (𝐴 = ∅ → 𝐴 = ∪ 𝐴) |
15 | limuni 6036 | . . 3 ⊢ (Lim 𝐴 → 𝐴 = ∪ 𝐴) | |
16 | 14, 15 | jaoi 846 | . 2 ⊢ ((𝐴 = ∅ ∨ Lim 𝐴) → 𝐴 = ∪ 𝐴) |
17 | 9, 16 | impbid1 217 | 1 ⊢ (Ord 𝐴 → (𝐴 = ∪ 𝐴 ↔ (𝐴 = ∅ ∨ Lim 𝐴))) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 ∧ wa 386 ∨ wo 836 ∧ w3a 1071 = wceq 1601 ≠ wne 2969 ∅c0 4141 ∪ cuni 4671 Ord word 5975 Lim wlim 5977 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1839 ax-4 1853 ax-5 1953 ax-6 2021 ax-7 2055 ax-9 2116 ax-10 2135 ax-11 2150 ax-12 2163 ax-13 2334 ax-ext 2754 |
This theorem depends on definitions: df-bi 199 df-an 387 df-or 837 df-3an 1073 df-tru 1605 df-ex 1824 df-nf 1828 df-sb 2012 df-clab 2764 df-cleq 2770 df-clel 2774 df-nfc 2921 df-ne 2970 df-ral 3095 df-rex 3096 df-v 3400 df-dif 3795 df-in 3799 df-ss 3806 df-nul 4142 df-sn 4399 df-uni 4672 df-lim 5981 |
This theorem is referenced by: ordzsl 7323 oeeulem 7965 cantnfp1lem2 8873 cantnflem1 8883 cnfcom2lem 8895 ordcmp 33029 |
Copyright terms: Public domain | W3C validator |