Metamath Proof Explorer

Theorem presucmap

Description: pre is really a predecessor (when it should be). This correctness theorem for pre makes it usable in proofs without unfolding iota . This theorem gives one witness; preuniqval gives it is the only one. (Contributed by Peter Mazsa, 12-Jan-2026)

Ref Expression
Assertion presucmap 
|- ( N e. ran SucMap -> pre N SucMap N )

Proof

Step Hyp Ref Expression
1 dfpre2 
 |-  ( N e. ran SucMap -> pre N = ( iota m m SucMap N ) )
2 1 eqcomd 
 |-  ( N e. ran SucMap -> ( iota m m SucMap N ) = pre N )
3 preex 
 |-  pre N e. _V
4 eupre2 
 |-  ( N e. ran SucMap -> ( N e. ran SucMap <-> E! m m SucMap N ) )
5 4 ibi 
 |-  ( N e. ran SucMap -> E! m m SucMap N )
6 breq1 
 |-  ( m = pre N -> ( m SucMap N <-> pre N SucMap N ) )
7 6 iota2 
 |-  ( ( pre N e. _V /\ E! m m SucMap N ) -> ( pre N SucMap N <-> ( iota m m SucMap N ) = pre N ) )
8 3 5 7 sylancr 
 |-  ( N e. ran SucMap -> ( pre N SucMap N <-> ( iota m m SucMap N ) = pre N ) )
9 2 8 mpbird 
 |-  ( N e. ran SucMap -> pre N SucMap N )