Metamath Proof Explorer

Theorem dfpre

Description: Alternate definition of the successor-predecessor. (Contributed by Peter Mazsa, 27-Jan-2026)

Ref Expression
Assertion dfpre 
|- pre N = ( iota m m e. Pred ( SucMap , _V , N ) )

Proof

Step Hyp Ref Expression
1 df-pre 
 |-  pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) )
2 dmsucmap 
 |-  dom SucMap = _V
3 predeq2 
 |-  ( dom SucMap = _V -> Pred ( SucMap , dom SucMap , N ) = Pred ( SucMap , _V , N ) )
4 2 3 ax-mp 
 |-  Pred ( SucMap , dom SucMap , N ) = Pred ( SucMap , _V , N )
5 4 eleq2i 
 |-  ( m e. Pred ( SucMap , dom SucMap , N ) <-> m e. Pred ( SucMap , _V , N ) )
6 5 iotabii 
 |-  ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) = ( iota m m e. Pred ( SucMap , _V , N ) )
7 1 6 eqtri 
 |-  pre N = ( iota m m e. Pred ( SucMap , _V , N ) )