Metamath Proof Explorer

Theorem preex

Description: The successor-predecessor exists. (Contributed by Peter Mazsa, 12-Jan-2026)

Ref Expression
Assertion preex 
|- pre N e. _V

Proof

Step Hyp Ref Expression
1 df-pre 
 |-  pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) )
2 iotaex 
 |-  ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) e. _V
3 1 2 eqeltri 
 |-  pre N e. _V