Theorem elom3

Description: A simplification of elom assuming the Axiom of Infinity. (Contributed by NM, 30-May-2003)

	Ref	Expression
Assertion	elom3	$$⊢A\in \mathrm{\omega }\leftrightarrow \forall x\left(\mathrm{Lim}x\to A\in x\right)$$

Proof

Step	Hyp	Ref	Expression
1		elom	$$⊢A\in \mathrm{\omega }\leftrightarrow \left(A\in \mathrm{On}\wedge \forall x\left(\mathrm{Lim}x\to A\in x\right)\right)$$
2		limom	$$⊢\mathrm{Lim}\mathrm{\omega }$$
3		omex	$$⊢\mathrm{\omega }\in \mathrm{V}$$
4		limeq	$$⊢x=\mathrm{\omega }\to \left(\mathrm{Lim}x\leftrightarrow \mathrm{Lim}\mathrm{\omega }\right)$$
5		eleq2	$$⊢x=\mathrm{\omega }\to \left(A\in x\leftrightarrow A\in \mathrm{\omega }\right)$$
6	4 5	imbi12d	$$⊢x=\mathrm{\omega }\to \left(\left(\mathrm{Lim}x\to A\in x\right)\leftrightarrow \left(\mathrm{Lim}\mathrm{\omega }\to A\in \mathrm{\omega }\right)\right)$$
7	3 6	spcv	$$⊢\forall x\left(\mathrm{Lim}x\to A\in x\right)\to \left(\mathrm{Lim}\mathrm{\omega }\to A\in \mathrm{\omega }\right)$$
8	2 7	mpi	$$⊢\forall x\left(\mathrm{Lim}x\to A\in x\right)\to A\in \mathrm{\omega }$$
9		nnon	$$⊢A\in \mathrm{\omega }\to A\in \mathrm{On}$$
10	8 9	syl	$$⊢\forall x\left(\mathrm{Lim}x\to A\in x\right)\to A\in \mathrm{On}$$
11	10	pm4.71ri	$$⊢\forall x\left(\mathrm{Lim}x\to A\in x\right)\leftrightarrow \left(A\in \mathrm{On}\wedge \forall x\left(\mathrm{Lim}x\to A\in x\right)\right)$$
12	1 11	bitr4i	$$⊢A\in \mathrm{\omega }\leftrightarrow \forall x\left(\mathrm{Lim}x\to A\in x\right)$$