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 4054 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 4048  . 2 wff Lim A 
3  1  word 4046  . . 3 wff Ord A 
4  c0 3200  . . . 4 class ∅  
5  4, 1  wcel 1375  . . 3 wff ∅ ∈ A 
6  1  cuni 3553  . . . 4 class ∪ A 
7  1, 6  wceq 1228  . . 3 wff A = ∪ A 
8  3, 5, 7  w3a 873  . 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 4054 
Copyright terms: Public domain  W3C validator 