Theorem dfsucmap3 38486

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

Assertion

Ref	Expression
dfsucmap3	⊢ SucMap = ( I AdjLiftMap V)

Proof of Theorem dfsucmap3

Dummy variables 𝑛 𝑚 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqcom 2738	. . 3 ⊢ (𝑛 = suc 𝑚 ↔ suc 𝑚 = 𝑛)
2	1	opabbii 5156	. 2 ⊢ {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚} = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
3		df-adjliftmap 38480	. . 3 ⊢ ( I AdjLiftMap V) = (𝑚 ∈ dom (( I ∪ ◡ E ) ↾ V) ↦ [𝑚](( I ∪ ◡ E ) ↾ V))
4		dmresv 6147	. . . . 5 ⊢ dom (( I ∪ ◡ E ) ↾ V) = dom ( I ∪ ◡ E )
5		dmun 5849	. . . . . 6 ⊢ dom ( I ∪ ◡ E ) = (dom I ∪ dom ◡ E )
6		dmi 5860	. . . . . . 7 ⊢ dom I = V
7		dmcnvep 38422	. . . . . . 7 ⊢ dom ◡ E = (V ∖ {∅})
8	6, 7	uneq12i 4113	. . . . . 6 ⊢ (dom I ∪ dom ◡ E ) = (V ∪ (V ∖ {∅}))
9		undifabs 4425	. . . . . 6 ⊢ (V ∪ (V ∖ {∅})) = V
10	5, 8, 9	3eqtri 2758	. . . . 5 ⊢ dom ( I ∪ ◡ E ) = V
11	4, 10	eqtri 2754	. . . 4 ⊢ dom (( I ∪ ◡ E ) ↾ V) = V
12		orcom 870	. . . . . . 7 ⊢ ((𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚) ↔ (𝑛 ∈ 𝑚 ∨ 𝑛 ∈ {𝑚}))
13		elecALTV 38313	. . . . . . . . 9 ⊢ ((𝑚 ∈ V ∧ 𝑛 ∈ V) → (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑚( I ∪ ◡ E )𝑛))
14	13	el2v 3443	. . . . . . . 8 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑚( I ∪ ◡ E )𝑛)
15		brun 5140	. . . . . . . 8 ⊢ (𝑚( I ∪ ◡ E )𝑛 ↔ (𝑚 I 𝑛 ∨ 𝑚◡ E 𝑛))
16		equcom 2019	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 ↔ 𝑛 = 𝑚)
17		ideqg 5790	. . . . . . . . . . 11 ⊢ (𝑛 ∈ V → (𝑚 I 𝑛 ↔ 𝑚 = 𝑛))
18	17	elv 3441	. . . . . . . . . 10 ⊢ (𝑚 I 𝑛 ↔ 𝑚 = 𝑛)
19		velsn 4589	. . . . . . . . . 10 ⊢ (𝑛 ∈ {𝑚} ↔ 𝑛 = 𝑚)
20	16, 18, 19	3bitr4i 303	. . . . . . . . 9 ⊢ (𝑚 I 𝑛 ↔ 𝑛 ∈ {𝑚})
21		brcnvep 38312	. . . . . . . . . 10 ⊢ (𝑚 ∈ V → (𝑚◡ E 𝑛 ↔ 𝑛 ∈ 𝑚))
22	21	elv 3441	. . . . . . . . 9 ⊢ (𝑚◡ E 𝑛 ↔ 𝑛 ∈ 𝑚)
23	20, 22	orbi12i 914	. . . . . . . 8 ⊢ ((𝑚 I 𝑛 ∨ 𝑚◡ E 𝑛) ↔ (𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚))
24	14, 15, 23	3bitri 297	. . . . . . 7 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ (𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚))
25		elun 4100	. . . . . . 7 ⊢ (𝑛 ∈ (𝑚 ∪ {𝑚}) ↔ (𝑛 ∈ 𝑚 ∨ 𝑛 ∈ {𝑚}))
26	12, 24, 25	3bitr4i 303	. . . . . 6 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑛 ∈ (𝑚 ∪ {𝑚}))
27	26	eqriv 2728	. . . . 5 ⊢ [𝑚]( I ∪ ◡ E ) = (𝑚 ∪ {𝑚})
28		reli 5765	. . . . . . . 8 ⊢ Rel I
29		relcnv 6052	. . . . . . . 8 ⊢ Rel ◡ E
30		relun 5750	. . . . . . . 8 ⊢ (Rel ( I ∪ ◡ E ) ↔ (Rel I ∧ Rel ◡ E ))
31	28, 29, 30	mpbir2an 711	. . . . . . 7 ⊢ Rel ( I ∪ ◡ E )
32		dfrel3 6145	. . . . . . 7 ⊢ (Rel ( I ∪ ◡ E ) ↔ (( I ∪ ◡ E ) ↾ V) = ( I ∪ ◡ E ))
33	31, 32	mpbi 230	. . . . . 6 ⊢ (( I ∪ ◡ E ) ↾ V) = ( I ∪ ◡ E )
34	33	eceq2i 8664	. . . . 5 ⊢ [𝑚](( I ∪ ◡ E ) ↾ V) = [𝑚]( I ∪ ◡ E )
35		df-suc 6312	. . . . 5 ⊢ suc 𝑚 = (𝑚 ∪ {𝑚})
36	27, 34, 35	3eqtr4i 2764	. . . 4 ⊢ [𝑚](( I ∪ ◡ E ) ↾ V) = suc 𝑚
37	11, 36	mpteq12i 5186	. . 3 ⊢ (𝑚 ∈ dom (( I ∪ ◡ E ) ↾ V) ↦ [𝑚](( I ∪ ◡ E ) ↾ V)) = (𝑚 ∈ V ↦ suc 𝑚)
38		mptv 5195	. . 3 ⊢ (𝑚 ∈ V ↦ suc 𝑚) = {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚}
39	3, 37, 38	3eqtri 2758	. 2 ⊢ ( I AdjLiftMap V) = {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚}
40		df-sucmap 38485	. 2 ⊢ SucMap = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
41	2, 39, 40	3eqtr4ri 2765	1 ⊢ SucMap = ( I AdjLiftMap V)

Syntax hints:   ↔ wb 206   ∨ wo 847   = wceq 1541   ∈ wcel 2111  Vcvv 3436   ∖ cdif 3894   ∪ cun 3895  ∅c0 4280  {csn 4573   class class class wbr 5089  {copab 5151   ↦ cmpt 5170   I cid 5508   E cep 5513  ^◡ccnv 5613  dom cdm 5614   ↾ cres 5616  Rel wrel 5619  suc csuc 6308  [cec 8620   AdjLiftMap cadjliftmap 38225   SucMap csucmap 38227

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-12 2180  ax-ext 2703  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4281  df-if 4473  df-sn 4574  df-pr 4576  df-op 4580  df-br 5090  df-opab 5152  df-mpt 5171  df-id 5509  df-eprel 5514  df-xp 5620  df-rel 5621  df-cnv 5622  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627  df-suc 6312  df-ec 8624  df-adjliftmap 38480  df-sucmap 38485

This theorem is referenced by:  dfsucmap2  38487