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		dfadjliftmap	⊢ ( I AdjLiftMap dom I ) = ( 𝑚 ∈ dom ( ( I ∪ ◡ E ) ↾ dom I ) ↦ [ 𝑚 ] ( ( I ∪ ◡ E ) ↾ dom I ) )
8		dfadjliftmap	⊢ ( 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 )