Metamath Proof Explorer


Theorem peano1OLD

Description: Obsolete version of peano1 as of 29-Nov-2024. (Contributed by NM, 15-May-1994) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion peano1OLD
|- (/) e. _om

Proof

Step Hyp Ref Expression
1 limom
 |-  Lim _om
2 0ellim
 |-  ( Lim _om -> (/) e. _om )
3 1 2 ax-mp
 |-  (/) e. _om