| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > df-lim | Structured version Visualization version GIF version | ||
| Description: Define the limit ordinal predicate, which is true for a nonempty ordinal that is not a successor (i.e. that is the union of itself). Our definition combines the definition of Lim of [BellMachover] p. 471 and Exercise 1 of [TakeutiZaring] p. 42. See dflim2 6441, dflim3 7868, and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994.) |
| Ref | Expression |
|---|---|
| df-lim | ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | cA | . . 3 class 𝐴 | |
| 2 | 1 | wlim 6385 | . 2 wff Lim 𝐴 |
| 3 | 1 | word 6383 | . . 3 wff Ord 𝐴 |
| 4 | c0 4333 | . . . 4 class ∅ | |
| 5 | 1, 4 | wne 2940 | . . 3 wff 𝐴 ≠ ∅ |
| 6 | 1 | cuni 4907 | . . . 4 class ∪ 𝐴 |
| 7 | 1, 6 | wceq 1540 | . . 3 wff 𝐴 = ∪ 𝐴 |
| 8 | 3, 5, 7 | w3a 1087 | . 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) |
| 9 | 2, 8 | wb 206 | 1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) |
| Colors of variables: wff setvar class |
| This definition is referenced by: limeq 6396 dflim2 6441 limord 6444 limuni 6445 unizlim 6507 limon 7856 dflim3 7868 nnsuc 7905 onfununi 8381 nlim1 8527 nlim2 8528 dfrdg2 35796 ellimits 35911 onsucuni3 37368 omlimcl2 43254 dflim5 43342 |
| Copyright terms: Public domain | W3C validator |