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.) 
Ref  Expression 

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

1  cA  . . 3 class A  
2  1  wlim 4025  . 2 wff Lim A 
3  1  word 4023  . . 3 wff Ord A 
4  c0 3202  . . . 4 class ∅  
5  4, 1  wcel 1375  . . 3 wff ∅ ∈ A 
6  1  cuni 3532  . . . 4 class ∪ A 
7  1, 6  wceq 1373  . . 3 wff A = ∪ A 
8  3, 5, 7  w3a 875  . 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 4030 limom 4232 
Copyright terms: Public domain  W3C validator 