Theorem dfsucmap3

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

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

Proof

Step	Hyp	Ref	Expression
1		eqcom	$$⊢n=\mathrm{suc}m\leftrightarrow \mathrm{suc}m=n$$
2	1	opabbii	$$⊢\left\{⟨m,n⟩|n=\mathrm{suc}m\right\}=\left\{⟨m,n⟩|\mathrm{suc}m=n\right\}$$
3		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 |-
4		dmresv	$$⊢\mathrm{dom}\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{V}}\right)=\mathrm{dom}\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)$$
5		dmun	$$⊢\mathrm{dom}\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)=\mathrm{dom}\mathrm{I}\cup \mathrm{dom}{\mathrm{E}}^{-1}$$
6		dmi	$$⊢\mathrm{dom}\mathrm{I}=\mathrm{V}$$
7		dmcnvep	$$⊢\mathrm{dom}{\mathrm{E}}^{-1}=\mathrm{V}\setminus \left\{\varnothing \right\}$$
8	6 7	uneq12i	$$⊢\mathrm{dom}\mathrm{I}\cup \mathrm{dom}{\mathrm{E}}^{-1}=\mathrm{V}\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)$$
9		undifabs	$$⊢\mathrm{V}\cup \left(\mathrm{V}\setminus \left\{\varnothing \right\}\right)=\mathrm{V}$$
10	5 8 9	3eqtri	$$⊢\mathrm{dom}\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)=\mathrm{V}$$
11	4 10	eqtri	$$⊢\mathrm{dom}\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{V}}\right)=\mathrm{V}$$
12		orcom	$$⊢\left(n\in \left\{m\right\}\vee n\in m\right)\leftrightarrow \left(n\in m\vee n\in \left\{m\right\}\right)$$
13		elecALTV	$$⊢\left(m\in \mathrm{V}\wedge n\in \mathrm{V}\right)\to \left(n\in \left[m\right]\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\leftrightarrow m\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)n\right)$$
14	13	el2v	$$⊢n\in \left[m\right]\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\leftrightarrow m\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)n$$
15		brun	$$⊢m\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)n\leftrightarrow \left(m\mathrm{I}n\vee m{\mathrm{E}}^{-1}n\right)$$
16		equcom	$$⊢m=n\leftrightarrow n=m$$
17		ideqg	$$⊢n\in \mathrm{V}\to \left(m\mathrm{I}n\leftrightarrow m=n\right)$$
18	17	elv	$$⊢m\mathrm{I}n\leftrightarrow m=n$$
19		velsn	$$⊢n\in \left\{m\right\}\leftrightarrow n=m$$
20	16 18 19	3bitr4i	$$⊢m\mathrm{I}n\leftrightarrow n\in \left\{m\right\}$$
21		brcnvep	$$⊢m\in \mathrm{V}\to \left(m{\mathrm{E}}^{-1}n\leftrightarrow n\in m\right)$$
22	21	elv	$$⊢m{\mathrm{E}}^{-1}n\leftrightarrow n\in m$$
23	20 22	orbi12i	$$⊢\left(m\mathrm{I}n\vee m{\mathrm{E}}^{-1}n\right)\leftrightarrow \left(n\in \left\{m\right\}\vee n\in m\right)$$
24	14 15 23	3bitri	$$⊢n\in \left[m\right]\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\leftrightarrow \left(n\in \left\{m\right\}\vee n\in m\right)$$
25		elun	$$⊢n\in \left(m\cup \left\{m\right\}\right)\leftrightarrow \left(n\in m\vee n\in \left\{m\right\}\right)$$
26	12 24 25	3bitr4i	$$⊢n\in \left[m\right]\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\leftrightarrow n\in \left(m\cup \left\{m\right\}\right)$$
27	26	eqriv	$$⊢\left[m\right]\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)=m\cup \left\{m\right\}$$
28		reli	$$⊢\mathrm{Rel}\mathrm{I}$$
29		relcnv	$$⊢\mathrm{Rel}{\mathrm{E}}^{-1}$$
30		relun	$$⊢\mathrm{Rel}\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\leftrightarrow \left(\mathrm{Rel}\mathrm{I}\wedge \mathrm{Rel}{\mathrm{E}}^{-1}\right)$$
31	28 29 30	mpbir2an	$$⊢\mathrm{Rel}\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)$$
32		dfrel3	$$⊢\mathrm{Rel}\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\leftrightarrow {\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{V}}=\mathrm{I}\cup {\mathrm{E}}^{-1}$$
33	31 32	mpbi	$$⊢{\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{V}}=\mathrm{I}\cup {\mathrm{E}}^{-1}$$
34	33	eceq2i	$$⊢\left[m\right]\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{V}}\right)=\left[m\right]\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)$$
35		df-suc	$$⊢\mathrm{suc}m=m\cup \left\{m\right\}$$
36	27 34 35	3eqtr4i	$$⊢\left[m\right]\left({\left(\mathrm{I}\cup {\mathrm{E}}^{-1}\right)\upharpoonright }_{\mathrm{V}}\right)=\mathrm{suc}m$$
37	11 36	mpteq12i	$$⊢\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)=\left(m\in \mathrm{V}⟼\mathrm{suc}m\right)$$
38		mptv	$$⊢\left(m\in \mathrm{V}⟼\mathrm{suc}m\right)=\left\{⟨m,n⟩|n=\mathrm{suc}m\right\}$$
39	3 37 38	3eqtri	Could not format ( _I AdjLiftMap _V ) = { <. m , n >. | n = suc m } : No typesetting found for |- ( _I AdjLiftMap _V ) = { <. m , n >. | n = suc m } with typecode |-
40		df-sucmap	Could not format SucMap = { <. m , n >. | suc m = n } : No typesetting found for |- SucMap = { <. m , n >. | suc m = n } with typecode |-
41	2 39 40	3eqtr4ri	Could not format SucMap = ( _I AdjLiftMap _V ) : No typesetting found for |- SucMap = ( _I AdjLiftMap _V ) with typecode |-