# Metamath Proof Explorer

## Definition df-lim

Description: Define the limit ordinal predicate, which is true for a nonempty ordinal that 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. See dflim2 , dflim3 , and dflim4 for alternate definitions. (Contributed by NM, 22-Apr-1994)

Ref Expression
Assertion df-lim ${⊢}\mathrm{Lim}{A}↔\left(\mathrm{Ord}{A}\wedge {A}\ne \varnothing \wedge {A}=\bigcup {A}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cA ${class}{A}$
1 0 wlim ${wff}\mathrm{Lim}{A}$
2 0 word ${wff}\mathrm{Ord}{A}$
3 c0 ${class}\varnothing$
4 0 3 wne ${wff}{A}\ne \varnothing$
5 0 cuni ${class}\bigcup {A}$
6 0 5 wceq ${wff}{A}=\bigcup {A}$
7 2 4 6 w3a ${wff}\left(\mathrm{Ord}{A}\wedge {A}\ne \varnothing \wedge {A}=\bigcup {A}\right)$
8 1 7 wb ${wff}\left(\mathrm{Lim}{A}↔\left(\mathrm{Ord}{A}\wedge {A}\ne \varnothing \wedge {A}=\bigcup {A}\right)\right)$