Theorem dfsucmap3 38784

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 2743	. . 3 ⊢ (𝑛 = suc 𝑚 ↔ suc 𝑚 = 𝑛)
2	1	opabbii 5152	. 2 ⊢ {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚} = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
3		dfadjliftmap 38777	. . 3 ⊢ ( I AdjLiftMap V) = (𝑚 ∈ dom (( I ∪ ◡ E ) ↾ V) ↦ [𝑚](( I ∪ ◡ E ) ↾ V))
4		dmresv 6164	. . . . 5 ⊢ dom (( I ∪ ◡ E ) ↾ V) = dom ( I ∪ ◡ E )
5		dmun 5865	. . . . . 6 ⊢ dom ( I ∪ ◡ E ) = (dom I ∪ dom ◡ E )
6		dmi 5876	. . . . . . 7 ⊢ dom I = V
7		dmcnvep 38709	. . . . . . 7 ⊢ dom ◡ E = (V ∖ {∅})
8	6, 7	uneq12i 4106	. . . . . 6 ⊢ (dom I ∪ dom ◡ E ) = (V ∪ (V ∖ {∅}))
9		undifabs 4418	. . . . . 6 ⊢ (V ∪ (V ∖ {∅})) = V
10	5, 8, 9	3eqtri 2763	. . . . 5 ⊢ dom ( I ∪ ◡ E ) = V
11	4, 10	eqtri 2759	. . . 4 ⊢ dom (( I ∪ ◡ E ) ↾ V) = V
12		orcom 871	. . . . . . 7 ⊢ ((𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚) ↔ (𝑛 ∈ 𝑚 ∨ 𝑛 ∈ {𝑚}))
13		elecALTV 38592	. . . . . . . . 9 ⊢ ((𝑚 ∈ V ∧ 𝑛 ∈ V) → (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑚( I ∪ ◡ E )𝑛))
14	13	el2v 3436	. . . . . . . 8 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑚( I ∪ ◡ E )𝑛)
15		brun 5136	. . . . . . . 8 ⊢ (𝑚( I ∪ ◡ E )𝑛 ↔ (𝑚 I 𝑛 ∨ 𝑚◡ E 𝑛))
16		equcom 2020	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 ↔ 𝑛 = 𝑚)
17		ideqg 5806	. . . . . . . . . . 11 ⊢ (𝑛 ∈ V → (𝑚 I 𝑛 ↔ 𝑚 = 𝑛))
18	17	elv 3434	. . . . . . . . . 10 ⊢ (𝑚 I 𝑛 ↔ 𝑚 = 𝑛)
19		velsn 4583	. . . . . . . . . 10 ⊢ (𝑛 ∈ {𝑚} ↔ 𝑛 = 𝑚)
20	16, 18, 19	3bitr4i 303	. . . . . . . . 9 ⊢ (𝑚 I 𝑛 ↔ 𝑛 ∈ {𝑚})
21		brcnvep 38591	. . . . . . . . . 10 ⊢ (𝑚 ∈ V → (𝑚◡ E 𝑛 ↔ 𝑛 ∈ 𝑚))
22	21	elv 3434	. . . . . . . . 9 ⊢ (𝑚◡ E 𝑛 ↔ 𝑛 ∈ 𝑚)
23	20, 22	orbi12i 915	. . . . . . . 8 ⊢ ((𝑚 I 𝑛 ∨ 𝑚◡ E 𝑛) ↔ (𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚))
24	14, 15, 23	3bitri 297	. . . . . . 7 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ (𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚))
25		elun 4093	. . . . . . 7 ⊢ (𝑛 ∈ (𝑚 ∪ {𝑚}) ↔ (𝑛 ∈ 𝑚 ∨ 𝑛 ∈ {𝑚}))
26	12, 24, 25	3bitr4i 303	. . . . . 6 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑛 ∈ (𝑚 ∪ {𝑚}))
27	26	eqriv 2733	. . . . 5 ⊢ [𝑚]( I ∪ ◡ E ) = (𝑚 ∪ {𝑚})
28		reli 5782	. . . . . . . 8 ⊢ Rel I
29		relcnv 6069	. . . . . . . 8 ⊢ Rel ◡ E
30		relun 5767	. . . . . . . 8 ⊢ (Rel ( I ∪ ◡ E ) ↔ (Rel I ∧ Rel ◡ E ))
31	28, 29, 30	mpbir2an 712	. . . . . . 7 ⊢ Rel ( I ∪ ◡ E )
32		dfrel3 6162	. . . . . . 7 ⊢ (Rel ( I ∪ ◡ E ) ↔ (( I ∪ ◡ E ) ↾ V) = ( I ∪ ◡ E ))
33	31, 32	mpbi 230	. . . . . 6 ⊢ (( I ∪ ◡ E ) ↾ V) = ( I ∪ ◡ E )
34	33	eceq2i 8686	. . . . 5 ⊢ [𝑚](( I ∪ ◡ E ) ↾ V) = [𝑚]( I ∪ ◡ E )
35		df-suc 6329	. . . . 5 ⊢ suc 𝑚 = (𝑚 ∪ {𝑚})
36	27, 34, 35	3eqtr4i 2769	. . . 4 ⊢ [𝑚](( I ∪ ◡ E ) ↾ V) = suc 𝑚
37	11, 36	mpteq12i 5182	. . 3 ⊢ (𝑚 ∈ dom (( I ∪ ◡ E ) ↾ V) ↦ [𝑚](( I ∪ ◡ E ) ↾ V)) = (𝑚 ∈ V ↦ suc 𝑚)
38		mptv 5191	. . 3 ⊢ (𝑚 ∈ V ↦ suc 𝑚) = {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚}
39	3, 37, 38	3eqtri 2763	. 2 ⊢ ( I AdjLiftMap V) = {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚}
40		df-sucmap 38783	. 2 ⊢ SucMap = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
41	2, 39, 40	3eqtr4ri 2770	1 ⊢ SucMap = ( I AdjLiftMap V)

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1542   ∈ wcel 2114  Vcvv 3429   ∖ cdif 3886   ∪ cun 3887  ∅c0 4273  {csn 4567   class class class wbr 5085  {copab 5147   ↦ cmpt 5166   I cid 5525   E cep 5530  ^◡ccnv 5630  dom cdm 5631   ↾ cres 5633  Rel wrel 5636  suc csuc 6325  [cec 8641   AdjLiftMap cadjliftmap 38497   SucMap csucmap 38499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-pr 5375

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-eprel 5531  df-xp 5637  df-rel 5638  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-suc 6329  df-ec 8645  df-qmap 38767  df-adjliftmap 38776  df-sucmap 38783

This theorem is referenced by:  dfsucmap2  38785