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

Definition df-ilim 4172
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  (/)  e.  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 4173 instead for naming consistency with set.mm. (New usage is discouraged.)
Assertion
Ref Expression
df-ilim  |-  ( Lim 
A  <->  ( Ord  A  /\  (/)  e.  A  /\  A  =  U. A ) )

Detailed syntax breakdown of Definition df-ilim
StepHypRef Expression
1 cA . . 3  class  A
21wlim 4167 . 2  wff  Lim  A
31word 4165 . . 3  wff  Ord  A
4 c0 3275 . . . 4  class  (/)
54, 1wcel 1436 . . 3  wff  (/)  e.  A
61cuni 3638 . . . 4  class  U. A
71, 6wceq 1287 . . 3  wff  A  = 
U. A
83, 5, 7w3a 922 . 2  wff  ( Ord 
A  /\  (/)  e.  A  /\  A  =  U. A )
92, 8wb 103 1  wff  ( Lim 
A  <->  ( Ord  A  /\  (/)  e.  A  /\  A  =  U. A ) )
Colors of variables: wff set class
This definition is referenced by:  dflim2  4173
  Copyright terms: Public domain W3C validator