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 
|- ( A e. _om <-> A. x ( Lim x -> A e. x ) )

Proof

Step Hyp Ref Expression
1 elom 
 |-  ( A e. _om <-> ( A e. On /\ A. x ( Lim x -> A e. x ) ) )
2 limom 
 |-  Lim _om
3 omex 
 |-  _om e. _V
4 limeq 
 |-  ( x = _om -> ( Lim x <-> Lim _om ) )
5 eleq2 
 |-  ( x = _om -> ( A e. x <-> A e. _om ) )
6 4 5 imbi12d 
 |-  ( x = _om -> ( ( Lim x -> A e. x ) <-> ( Lim _om -> A e. _om ) ) )
7 3 6 spcv 
 |-  ( A. x ( Lim x -> A e. x ) -> ( Lim _om -> A e. _om ) )
8 2 7 mpi 
 |-  ( A. x ( Lim x -> A e. x ) -> A e. _om )
9 nnon 
 |-  ( A e. _om -> A e. On )
10 8 9 syl 
 |-  ( A. x ( Lim x -> A e. x ) -> A e. On )
11 10 pm4.71ri 
 |-  ( A. x ( Lim x -> A e. x ) <-> ( A e. On /\ A. x ( Lim x -> A e. x ) ) )
12 1 11 bitr4i 
 |-  ( A e. _om <-> A. x ( Lim x -> A e. x ) )