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 
|- ( N e. V -> pre N = ( iota m m e. [ N ] `' SucMap ) )

Proof

Step Hyp Ref Expression
1 df-pre 
 |-  pre N = ( iota m m e. Pred ( SucMap , dom SucMap , N ) )
2 dfpred4 
 |-  ( N e. V -> Pred ( SucMap , dom SucMap , N ) = [ N ] `' ( SucMap |` dom SucMap ) )
3 relsucmap 
 |-  Rel SucMap
4 dfrel5 
 |-  ( Rel SucMap <-> ( SucMap |` dom SucMap ) = SucMap )
5 3 4 mpbi 
 |-  ( SucMap |` dom SucMap ) = SucMap
6 5 cnveqi 
 |-  `' ( SucMap |` dom SucMap ) = `' SucMap
7 6 eceq2i 
 |-  [ N ] `' ( SucMap |` dom SucMap ) = [ N ] `' SucMap
8 2 7 eqtrdi 
 |-  ( N e. V -> Pred ( SucMap , dom SucMap , N ) = [ N ] `' SucMap )
9 8 eleq2d 
 |-  ( N e. V -> ( m e. Pred ( SucMap , dom SucMap , N ) <-> m e. [ N ] `' SucMap ) )
10 9 iotabidv 
 |-  ( N e. V -> ( iota m m e. Pred ( SucMap , dom SucMap , N ) ) = ( iota m m e. [ N ] `' SucMap ) )
11 1 10 eqtrid 
 |-  ( N e. V -> pre N = ( iota m m e. [ N ] `' SucMap ) )