Intuitionistic Logic Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > ILE Home > Th. List > dfilim  Structured version 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 A ≠ ∅ to ∅ ∈ A (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 4072 instead for naming consistency with set.mm. (New usage is discouraged.) 
Ref  Expression 

dfilim  ⊢ (Lim A ↔ (Ord A ∧ ∅ ∈ A ∧ A = ∪ A)) 
Step  Hyp  Ref  Expression 

1  cA  . . 3 class A  
2  1  wlim 4066  . 2 wff Lim A 
3  1  word 4064  . . 3 wff Ord A 
4  c0 3218  . . . 4 class ∅  
5  4, 1  wcel 1390  . . 3 wff ∅ ∈ A 
6  1  cuni 3570  . . . 4 class ∪ A 
7  1, 6  wceq 1242  . . 3 wff A = ∪ A 
8  3, 5, 7  w3a 884  . 2 wff (Ord A ∧ ∅ ∈ A ∧ A = ∪ A) 
9  2, 8  wb 98  1 wff (Lim A ↔ (Ord A ∧ ∅ ∈ A ∧ A = ∪ A)) 
Colors of variables: wff set class 
This definition is referenced by: dflim2 4072 
Copyright terms: Public domain  W3C validator 