![]() |
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 6418, dflim3 7832, 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 6362 | . 2 wff Lim 𝐴 |
3 | 1 | word 6360 | . . 3 wff Ord 𝐴 |
4 | c0 4321 | . . . 4 class ∅ | |
5 | 1, 4 | wne 2940 | . . 3 wff 𝐴 ≠ ∅ |
6 | 1 | cuni 4907 | . . . 4 class ∪ 𝐴 |
7 | 1, 6 | wceq 1541 | . . 3 wff 𝐴 = ∪ 𝐴 |
8 | 3, 5, 7 | w3a 1087 | . 2 wff (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴) |
9 | 2, 8 | wb 205 | 1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ 𝐴 ≠ ∅ ∧ 𝐴 = ∪ 𝐴)) |
Colors of variables: wff setvar class |
This definition is referenced by: limeq 6373 dflim2 6418 limord 6421 limuni 6422 unizlim 6484 limon 7820 dflim3 7832 nnsuc 7869 onfununi 8337 nlim1 8485 nlim2 8486 dfrdg2 34755 ellimits 34870 onsucuni3 36236 omlimcl2 41976 dflim5 42064 |
Copyright terms: Public domain | W3C validator |