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 Could not format assertion : No typesetting found for |- ( N e. ran SucMap -> pre N SucMap N ) with typecode |-

Proof

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