elom3

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

		Ref	Expression
	Assertion	elom3	$⊢ A \in ω \leftrightarrow \forall x (Lim x \to A \in x)$

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

Metamath Proof Explorer