![]() |
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 6420, dflim3 7838, 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 6364 | . 2 wff Lim 𝐴 |
3 | 1 | word 6362 | . . 3 wff Ord 𝐴 |
4 | c0 4321 | . . . 4 class ∅ | |
5 | 1, 4 | wne 2938 | . . 3 wff 𝐴 ≠ ∅ |
6 | 1 | cuni 4907 | . . . 4 class ∪ 𝐴 |
7 | 1, 6 | wceq 1539 | . . 3 wff 𝐴 = ∪ 𝐴 |
8 | 3, 5, 7 | w3a 1085 | . 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) |
9 | 2, 8 | wb 205 | 1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: limeq 6375 dflim2 6420 limord 6423 limuni 6424 unizlim 6486 limon 7826 dflim3 7838 nnsuc 7875 onfununi 8343 nlim1 8491 nlim2 8492 dfrdg2 35071 ellimits 35186 onsucuni3 36551 omlimcl2 42293 dflim5 42381 |
Copyright terms: Public domain | W3C validator |