This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑥 → 𝐴 ∈ 𝑥 ) )