Theorem dfsucmap3 38714

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 2744	. . 3 ⊢ (𝑛 = suc 𝑚 ↔ suc 𝑚 = 𝑛)
2	1	opabbii 5167	. 2 ⊢ {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚} = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
3		dfadjliftmap 38707	. . 3 ⊢ ( I AdjLiftMap V) = (𝑚 ∈ dom (( I ∪ ◡ E ) ↾ V) ↦ [𝑚](( I ∪ ◡ E ) ↾ V))
4		dmresv 6166	. . . . 5 ⊢ dom (( I ∪ ◡ E ) ↾ V) = dom ( I ∪ ◡ E )
5		dmun 5867	. . . . . 6 ⊢ dom ( I ∪ ◡ E ) = (dom I ∪ dom ◡ E )
6		dmi 5878	. . . . . . 7 ⊢ dom I = V
7		dmcnvep 38639	. . . . . . 7 ⊢ dom ◡ E = (V ∖ {∅})
8	6, 7	uneq12i 4120	. . . . . 6 ⊢ (dom I ∪ dom ◡ E ) = (V ∪ (V ∖ {∅}))
9		undifabs 4432	. . . . . 6 ⊢ (V ∪ (V ∖ {∅})) = V
10	5, 8, 9	3eqtri 2764	. . . . 5 ⊢ dom ( I ∪ ◡ E ) = V
11	4, 10	eqtri 2760	. . . 4 ⊢ dom (( I ∪ ◡ E ) ↾ V) = V
12		orcom 871	. . . . . . 7 ⊢ ((𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚) ↔ (𝑛 ∈ 𝑚 ∨ 𝑛 ∈ {𝑚}))
13		elecALTV 38522	. . . . . . . . 9 ⊢ ((𝑚 ∈ V ∧ 𝑛 ∈ V) → (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑚( I ∪ ◡ E )𝑛))
14	13	el2v 3449	. . . . . . . 8 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑚( I ∪ ◡ E )𝑛)
15		brun 5151	. . . . . . . 8 ⊢ (𝑚( I ∪ ◡ E )𝑛 ↔ (𝑚 I 𝑛 ∨ 𝑚◡ E 𝑛))
16		equcom 2020	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 ↔ 𝑛 = 𝑚)
17		ideqg 5808	. . . . . . . . . . 11 ⊢ (𝑛 ∈ V → (𝑚 I 𝑛 ↔ 𝑚 = 𝑛))
18	17	elv 3447	. . . . . . . . . 10 ⊢ (𝑚 I 𝑛 ↔ 𝑚 = 𝑛)
19		velsn 4598	. . . . . . . . . 10 ⊢ (𝑛 ∈ {𝑚} ↔ 𝑛 = 𝑚)
20	16, 18, 19	3bitr4i 303	. . . . . . . . 9 ⊢ (𝑚 I 𝑛 ↔ 𝑛 ∈ {𝑚})
21		brcnvep 38521	. . . . . . . . . 10 ⊢ (𝑚 ∈ V → (𝑚◡ E 𝑛 ↔ 𝑛 ∈ 𝑚))
22	21	elv 3447	. . . . . . . . 9 ⊢ (𝑚◡ E 𝑛 ↔ 𝑛 ∈ 𝑚)
23	20, 22	orbi12i 915	. . . . . . . 8 ⊢ ((𝑚 I 𝑛 ∨ 𝑚◡ E 𝑛) ↔ (𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚))
24	14, 15, 23	3bitri 297	. . . . . . 7 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ (𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚))
25		elun 4107	. . . . . . 7 ⊢ (𝑛 ∈ (𝑚 ∪ {𝑚}) ↔ (𝑛 ∈ 𝑚 ∨ 𝑛 ∈ {𝑚}))
26	12, 24, 25	3bitr4i 303	. . . . . 6 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑛 ∈ (𝑚 ∪ {𝑚}))
27	26	eqriv 2734	. . . . 5 ⊢ [𝑚]( I ∪ ◡ E ) = (𝑚 ∪ {𝑚})
28		reli 5783	. . . . . . . 8 ⊢ Rel I
29		relcnv 6071	. . . . . . . 8 ⊢ Rel ◡ E
30		relun 5768	. . . . . . . 8 ⊢ (Rel ( I ∪ ◡ E ) ↔ (Rel I ∧ Rel ◡ E ))
31	28, 29, 30	mpbir2an 712	. . . . . . 7 ⊢ Rel ( I ∪ ◡ E )
32		dfrel3 6164	. . . . . . 7 ⊢ (Rel ( I ∪ ◡ E ) ↔ (( I ∪ ◡ E ) ↾ V) = ( I ∪ ◡ E ))
33	31, 32	mpbi 230	. . . . . 6 ⊢ (( I ∪ ◡ E ) ↾ V) = ( I ∪ ◡ E )
34	33	eceq2i 8688	. . . . 5 ⊢ [𝑚](( I ∪ ◡ E ) ↾ V) = [𝑚]( I ∪ ◡ E )
35		df-suc 6331	. . . . 5 ⊢ suc 𝑚 = (𝑚 ∪ {𝑚})
36	27, 34, 35	3eqtr4i 2770	. . . 4 ⊢ [𝑚](( I ∪ ◡ E ) ↾ V) = suc 𝑚
37	11, 36	mpteq12i 5197	. . 3 ⊢ (𝑚 ∈ dom (( I ∪ ◡ E ) ↾ V) ↦ [𝑚](( I ∪ ◡ E ) ↾ V)) = (𝑚 ∈ V ↦ suc 𝑚)
38		mptv 5206	. . 3 ⊢ (𝑚 ∈ V ↦ suc 𝑚) = {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚}
39	3, 37, 38	3eqtri 2764	. 2 ⊢ ( I AdjLiftMap V) = {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚}
40		df-sucmap 38713	. 2 ⊢ SucMap = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
41	2, 39, 40	3eqtr4ri 2771	1 ⊢ SucMap = ( I AdjLiftMap V)

Syntax hints:   ↔ wb 206   ∨ wo 848   = wceq 1542   ∈ wcel 2114  Vcvv 3442   ∖ cdif 3900   ∪ cun 3901  ∅c0 4287  {csn 4582   class class class wbr 5100  {copab 5162   ↦ cmpt 5181   I cid 5526   E cep 5531  ^◡ccnv 5631  dom cdm 5632   ↾ cres 5634  Rel wrel 5637  suc csuc 6327  [cec 8643   AdjLiftMap cadjliftmap 38427   SucMap csucmap 38429

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 2709  ax-sep 5243  ax-pr 5379

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 2716  df-cleq 2729  df-clel 2812  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5527  df-eprel 5532  df-xp 5638  df-rel 5639  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-suc 6331  df-ec 8647  df-qmap 38697  df-adjliftmap 38706  df-sucmap 38713

This theorem is referenced by:  dfsucmap2  38715