Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-ilim GIF version

Definition df-ilim 4153
 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 4154 instead for naming consistency with set.mm. (New usage is discouraged.)
Assertion
Ref Expression
df-ilim (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴𝐴 = 𝐴))

Detailed syntax breakdown of Definition df-ilim
StepHypRef Expression
1 cA . . 3 class 𝐴
21wlim 4148 . 2 wff Lim 𝐴
31word 4146 . . 3 wff Ord 𝐴
4 c0 3268 . . . 4 class
54, 1wcel 1434 . . 3 wff ∅ ∈ 𝐴
61cuni 3622 . . . 4 class 𝐴
71, 6wceq 1285 . . 3 wff 𝐴 = 𝐴
83, 5, 7w3a 920 . 2 wff (Ord 𝐴 ∧ ∅ ∈ 𝐴𝐴 = 𝐴)
92, 8wb 103 1 wff (Lim 𝐴 ↔ (Ord 𝐴 ∧ ∅ ∈ 𝐴𝐴 = 𝐴))
 Colors of variables: wff set class This definition is referenced by:  dflim2  4154
 Copyright terms: Public domain W3C validator