![]() |
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 6442, dflim3 7867, 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 6386 | . 2 wff Lim 𝐴 |
3 | 1 | word 6384 | . . 3 wff Ord 𝐴 |
4 | c0 4338 | . . . 4 class ∅ | |
5 | 1, 4 | wne 2937 | . . 3 wff 𝐴 ≠ ∅ |
6 | 1 | cuni 4911 | . . . 4 class ∪ 𝐴 |
7 | 1, 6 | wceq 1536 | . . 3 wff 𝐴 = ∪ 𝐴 |
8 | 3, 5, 7 | w3a 1086 | . 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) |
9 | 2, 8 | wb 206 | 1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: limeq 6397 dflim2 6442 limord 6445 limuni 6446 unizlim 6508 limon 7855 dflim3 7867 nnsuc 7904 onfununi 8379 nlim1 8525 nlim2 8526 dfrdg2 35776 ellimits 35891 onsucuni3 37349 omlimcl2 43230 dflim5 43318 |
Copyright terms: Public domain | W3C validator |