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

Definition df-ilim 4029
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.)
Assertion
Ref Expression
df-ilim (Lim A ↔ (Ord A A A = A))

Detailed syntax breakdown of Definition df-ilim
StepHypRef Expression
1 cA . . 3 class A
21wlim 4025 . 2 wff Lim A
31word 4023 . . 3 wff Ord A
4 c0 3202 . . . 4 class
54, 1wcel 1375 . . 3 wff A
61cuni 3532 . . . 4 class A
71, 6wceq 1373 . . 3 wff A = A
83, 5, 7w3a 875 . 2 wff (Ord A A A = A)
92, 8wb 98 1 wff (Lim A ↔ (Ord A A A = A))
Colors of variables: wff set class
This definition is referenced by:  dflim2  4030  limom  4232
  Copyright terms: Public domain W3C validator