Theorem dfsucmap2

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

	Ref	Expression
Assertion	dfsucmap2	Could not format assertion : No typesetting found for |- SucMap = ( _I AdjLiftMap dom _I ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		dfsucmap3	Could not format SucMap = ( _I AdjLiftMap _V ) : No typesetting found for |- SucMap = ( _I AdjLiftMap _V ) with typecode |-
2		dmi	$$⊢\mathrm{dom}\mathrm{I}=\mathrm{V}$$
3	2	reseq2i	$$⊢{\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{dom}\mathrm{I}}={\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{V}}$$
4	3	dmeqi	$$⊢\mathrm{dom}\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{dom}\mathrm{I}}\right)=\mathrm{dom}\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{V}}\right)$$
5	3	eceq2i	$$⊢\left[m\right]\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{dom}\mathrm{I}}\right)=\left[m\right]\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{V}}\right)$$
6	4 5	mpteq12i	$$⊢\left(m\in \mathrm{dom}\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{dom}\mathrm{I}}\right)⟼\left[m\right]\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{dom}\mathrm{I}}\right)\right)=\left(m\in \mathrm{dom}\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{V}}\right)⟼\left[m\right]\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{V}}\right)\right)$$
7		dfadjliftmap	Could not format ( _I AdjLiftMap dom _I ) = ( m e. dom ( ( _I u. `' _E ) |` dom _I ) |-> [ m ] ( ( _I u. `' _E ) |` dom _I ) ) : No typesetting found for |- ( _I AdjLiftMap dom _I ) = ( m e. dom ( ( _I u. `' _E ) |` dom _I ) |-> [ m ] ( ( _I u. `' _E ) |` dom _I ) ) with typecode |-
8		dfadjliftmap	Could not format ( _I AdjLiftMap _V ) = ( m e. dom ( ( _I u. `' _E ) |` _V ) |-> [ m ] ( ( _I u. `' _E ) |` _V ) ) : No typesetting found for |- ( _I AdjLiftMap _V ) = ( m e. dom ( ( _I u. `' _E ) |` _V ) |-> [ m ] ( ( _I u. `' _E ) |` _V ) ) with typecode |-
9	6 7 8	3eqtr4i	Could not format ( _I AdjLiftMap dom _I ) = ( _I AdjLiftMap _V ) : No typesetting found for |- ( _I AdjLiftMap dom _I ) = ( _I AdjLiftMap _V ) with typecode |-
10	1 9	eqtr4i	Could not format SucMap = ( _I AdjLiftMap dom _I ) : No typesetting found for |- SucMap = ( _I AdjLiftMap dom _I ) with typecode |-