This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ∪ ◡ E ) ↾ dom I ) = ( ( I ∪ ◡ E ) ↾ V )
4 3 dmeqi ⊢ dom ( ( I ∪ ◡ E ) ↾ dom I ) = dom ( ( I ∪ ◡ E ) ↾ V )
5 3 eceq2i ⊢ [ 𝑚 ] ( ( I ∪ ◡ E ) ↾ dom I ) = [ 𝑚 ] ( ( I ∪ ◡ E ) ↾ V )
6 4 5 mpteq12i ⊢ ( 𝑚 ∈ dom ( ( I ∪ ◡ E ) ↾ dom I ) ↦ [ 𝑚 ] ( ( I ∪ ◡ E ) ↾ dom I ) ) = ( 𝑚 ∈ dom ( ( I ∪ ◡ E ) ↾ V ) ↦ [ 𝑚 ] ( ( I ∪ ◡ E ) ↾ V ) )
7 df-adjliftmap ⊢ ( I AdjLiftMap dom I ) = ( 𝑚 ∈ dom ( ( I ∪ ◡ E ) ↾ dom I ) ↦ [ 𝑚 ] ( ( I ∪ ◡ E ) ↾ dom I ) )
8 df-adjliftmap ⊢ ( I AdjLiftMap V ) = ( 𝑚 ∈ dom ( ( I ∪ ◡ E ) ↾ V ) ↦ [ 𝑚 ] ( ( I ∪ ◡ E ) ↾ V ) )
9 6 7 8 3eqtr4i ⊢ ( I AdjLiftMap dom I ) = ( I AdjLiftMap V )
10 1 9 eqtr4i ⊢ SucMap = ( I AdjLiftMap dom I )