Metamath Proof Explorer

Theorem dfsucmap2

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

Ref Expression
Assertion dfsucmap2 
|- SucMap = ( _I AdjLiftMap dom _I )

Proof

Step Hyp Ref Expression
1 dfsucmap3 
 |-  SucMap = ( _I AdjLiftMap _V )
2 dmi 
 |-  dom _I = _V
3 2 reseq2i 
 |-  ( ( _I u. `' _E ) |` dom _I ) = ( ( _I u. `' _E ) |` _V )
4 3 dmeqi 
 |-  dom ( ( _I u. `' _E ) |` dom _I ) = dom ( ( _I u. `' _E ) |` _V )
5 3 eceq2i 
 |-  [ m ] ( ( _I u. `' _E ) |` dom _I ) = [ m ] ( ( _I u. `' _E ) |` _V )
6 4 5 mpteq12i 
 |-  ( m e. dom ( ( _I u. `' _E ) |` dom _I ) |-> [ m ] ( ( _I u. `' _E ) |` dom _I ) ) = ( m e. dom ( ( _I u. `' _E ) |` _V ) |-> [ m ] ( ( _I u. `' _E ) |` _V ) )
7 df-adjliftmap 
 |-  ( _I AdjLiftMap dom _I ) = ( m e. dom ( ( _I u. `' _E ) |` dom _I ) |-> [ m ] ( ( _I u. `' _E ) |` dom _I ) )
8 df-adjliftmap 
 |-  ( _I AdjLiftMap _V ) = ( m e. dom ( ( _I u. `' _E ) |` _V ) |-> [ m ] ( ( _I u. `' _E ) |` _V ) )
9 6 7 8 3eqtr4i 
 |-  ( _I AdjLiftMap dom _I ) = ( _I AdjLiftMap _V )
10 1 9 eqtr4i 
 |-  SucMap = ( _I AdjLiftMap dom _I )