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 𝐴 ≠ ∅ to ∅ ∈ 𝐴 (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 4221 instead for naming consistency with set.mm. (New usage is discouraged.) |
Ref | Expression |
---|---|
df-ilim | ⊢ (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cA | . . 3 class 𝐴 | |
2 | 1 | wlim 4215 | . 2 wff Lim 𝐴 |
3 | 1 | word 4213 | . . 3 wff Ord 𝐴 |
4 | c0 3302 | . . . 4 class ∅ | |
5 | 4, 1 | wcel 1445 | . . 3 wff ∅ ∈ 𝐴 |
6 | 1 | cuni 3675 | . . . 4 class ∪ 𝐴 |
7 | 1, 6 | wceq 1296 | . . 3 wff 𝐴 = ∪ 𝐴 |
8 | 3, 5, 7 | w3a 927 | . 2 wff (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴) |
9 | 2, 8 | wb 104 | 1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴 ∧ 𝐴 = ∪ 𝐴)) |
Colors of variables: wff set class |
This definition is referenced by: dflim2 4221 |
Copyright terms: Public domain | W3C validator |