Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > dfilim  Structured version Unicode 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, 11Nov2018.) Use its alias dflim2 4073 instead for naming consistency with set.mm. (New usage is discouraged.) 
Ref  Expression 

dfilim 
Step  Hyp  Ref  Expression 

1  cA  . . 3  
2  1  wlim 4067  . 2 
3  1  word 4065  . . 3 
4  c0 3218  . . . 4  
5  4, 1  wcel 1390  . . 3 
6  1  cuni 3571  . . . 4 
7  1, 6  wceq 1242  . . 3 
8  3, 5, 7  w3a 884  . 2 
9  2, 8  wb 98  1 
Colors of variables: wff set class 
This definition is referenced by: dflim2 4073 
Copyright terms: Public domain  W3C validator 