Metamath Proof Explorer

Theorem dfpre

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

Ref Expression
Assertion dfpre Could not format assertion : No typesetting found for |- pre N = ( iota m m e. Pred ( SucMap , _V , N ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 df-pre Could not format pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) : No typesetting found for |- pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) with typecode |-
2 dmsucmap Could not format dom SucMap = _V : No typesetting found for |- dom SucMap = _V with typecode |-
3 predeq2 Could not format ( dom SucMap = _V -> Pred ( SucMap , dom SucMap , N ) = Pred ( SucMap , _V , N ) ) : No typesetting found for |- ( dom SucMap = _V -> Pred ( SucMap , dom SucMap , N ) = Pred ( SucMap , _V , N ) ) with typecode |-
4 2 3 ax-mp Could not format Pred ( SucMap , dom SucMap , N ) = Pred ( SucMap , _V , N ) : No typesetting found for |- Pred ( SucMap , dom SucMap , N ) = Pred ( SucMap , _V , N ) with typecode |-
5 4 eleq2i Could not format ( m e. Pred ( SucMap , dom SucMap , N ) <-> m e. Pred ( SucMap , _V , N ) ) : No typesetting found for |- ( m e. Pred ( SucMap , dom SucMap , N ) <-> m e. Pred ( SucMap , _V , N ) ) with typecode |-
6 5 iotabii Could not format ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) = ( iota m m e. Pred ( SucMap , _V , N ) ) : No typesetting found for |- ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) = ( iota m m e. Pred ( SucMap , _V , N ) ) with typecode |-
7 1 6 eqtri Could not format pre N = ( iota m m e. Pred ( SucMap , _V , N ) ) : No typesetting found for |- pre N = ( iota m m e. Pred ( SucMap , _V , N ) ) with typecode |-