Metamath Proof Explorer

Theorem dfpre4

Description: Alternate definition of the predecessor of the N set. The ` ``' SucMap ` is just the "PreMap"; we did not define it because we do not expect to use it extensively in future (cf. the comments of df-sucmap ). (Contributed by Peter Mazsa, 26-Jan-2026)

Ref Expression
Assertion dfpre4 Could not format assertion : No typesetting found for |- ( N e. V -> pre N = ( iota m m e. [ N ] `' SucMap ) ) 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 dfpred4 Could not format ( N e. V -> Pred ( SucMap , dom SucMap , N ) = [ N ] `' ( SucMap |` dom SucMap ) ) : No typesetting found for |- ( N e. V -> Pred ( SucMap , dom SucMap , N ) = [ N ] `' ( SucMap |` dom SucMap ) ) with typecode |-
3 relsucmap Could not format Rel SucMap : No typesetting found for |- Rel SucMap with typecode |-
4 dfrel5 Could not format ( Rel SucMap <-> ( SucMap |` dom SucMap ) = SucMap ) : No typesetting found for |- ( Rel SucMap <-> ( SucMap |` dom SucMap ) = SucMap ) with typecode |-
5 3 4 mpbi Could not format ( SucMap |` dom SucMap ) = SucMap : No typesetting found for |- ( SucMap |` dom SucMap ) = SucMap with typecode |-
6 5 cnveqi Could not format `' ( SucMap |` dom SucMap ) = `' SucMap : No typesetting found for |- `' ( SucMap |` dom SucMap ) = `' SucMap with typecode |-
7 6 eceq2i Could not format [ N ] `' ( SucMap |` dom SucMap ) = [ N ] `' SucMap : No typesetting found for |- [ N ] `' ( SucMap |` dom SucMap ) = [ N ] `' SucMap with typecode |-
8 2 7 eqtrdi Could not format ( N e. V -> Pred ( SucMap , dom SucMap , N ) = [ N ] `' SucMap ) : No typesetting found for |- ( N e. V -> Pred ( SucMap , dom SucMap , N ) = [ N ] `' SucMap ) with typecode |-
9 8 eleq2d Could not format ( N e. V -> ( m e. Pred ( SucMap , dom SucMap , N ) <-> m e. [ N ] `' SucMap ) ) : No typesetting found for |- ( N e. V -> ( m e. Pred ( SucMap , dom SucMap , N ) <-> m e. [ N ] `' SucMap ) ) with typecode |-
10 9 iotabidv Could not format ( N e. V -> ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) = ( iota m m e. [ N ] `' SucMap ) ) : No typesetting found for |- ( N e. V -> ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) = ( iota m m e. [ N ] `' SucMap ) ) with typecode |-
11 1 10 eqtrid Could not format ( N e. V -> pre N = ( iota m m e. [ N ] `' SucMap ) ) : No typesetting found for |- ( N e. V -> pre N = ( iota m m e. [ N ] `' SucMap ) ) with typecode |-