![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > df-ilim | GIF version |
Description: Define the limit ordinal predicate, which is true for an ordinal that has the empty set as an element and 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, and then changes A ≠ ∅ to ∅ ∈ A (which would be equivalent given the law of the excluded middle, but which is not for us). (Contributed by Jim Kingdon, 11-Nov-2018.) Use its alias dflim2 4073 instead for naming consistency with set.mm. (New usage is discouraged.) |
Ref | Expression |
---|---|
df-ilim | ⊢ (Lim A ↔ (Ord A ∧ ∅ ∈ A ∧ A = ∪ A)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class A | |
2 | 1 | wlim 4067 | . 2 wff Lim A |
3 | 1 | word 4065 | . . 3 wff Ord A |
4 | c0 3218 | . . . 4 class ∅ | |
5 | 4, 1 | wcel 1390 | . . 3 wff ∅ ∈ A |
6 | 1 | cuni 3571 | . . . 4 class ∪ A |
7 | 1, 6 | wceq 1242 | . . 3 wff A = ∪ A |
8 | 3, 5, 7 | w3a 884 | . 2 wff (Ord A ∧ ∅ ∈ A ∧ A = ∪ A) |
9 | 2, 8 | wb 98 | 1 wff (Lim A ↔ (Ord A ∧ ∅ ∈ A ∧ A = ∪ A)) |
Colors of variables: wff set class |
This definition is referenced by: dflim2 4073 |
Copyright terms: Public domain | W3C validator |