Theorem elom3

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

	Ref	Expression
Assertion	elom3	⊢ ( 𝐴 ∈ ω ↔ ∀ 𝑥 ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		elom	⊢ ( 𝐴 ∈ ω ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) ) )
2		limom	⊢ Lim ω
3		omex	⊢ ω ∈ V
4		limeq	⊢ ( 𝑥 = ω → ( Lim 𝑥 ↔ Lim ω ) )
5		eleq2	⊢ ( 𝑥 = ω → ( 𝐴 ∈ 𝑥 ↔ 𝐴 ∈ ω ) )
6	4 5	imbi12d	⊢ ( 𝑥 = ω → ( ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) ↔ ( Lim ω → 𝐴 ∈ ω ) ) )
7	3 6	spcv	⊢ ( ∀ 𝑥 ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) → ( Lim ω → 𝐴 ∈ ω ) )
8	2 7	mpi	⊢ ( ∀ 𝑥 ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) → 𝐴 ∈ ω )
9		nnon	⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
10	8 9	syl	⊢ ( ∀ 𝑥 ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) → 𝐴 ∈ On )
11	10	pm4.71ri	⊢ ( ∀ 𝑥 ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) ↔ ( 𝐴 ∈ On ∧ ∀ 𝑥 ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) ) )
12	1 11	bitr4i	⊢ ( 𝐴 ∈ ω ↔ ∀ 𝑥 ( Lim 𝑥 → 𝐴 ∈ 𝑥 ) )