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\leftrightarrow \left(\mathrm{Ord}A\wedge A\ne \varnothing \wedge A=\bigcup A\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cA	$$classA$$
1	0	wlim	$$wff\mathrm{Lim}A$$
2	0	word	$$wff\mathrm{Ord}A$$
3		c0	$$class\varnothing$$
4	0 3	wne	$$wffA\ne \varnothing$$
5	0	cuni	$$class\bigcup A$$
6	0 5	wceq	$$wffA=\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\leftrightarrow \left(\mathrm{Ord}A\wedge A\ne \varnothing \wedge A=\bigcup A\right)\right)$$