Theorem dfsucmap3 39532

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 2767	. . 3 ⊢ (𝑛 = suc 𝑚 ↔ suc 𝑚 = 𝑛)
2	1	opabbii 5171	. 2 ⊢ {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚} = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
3		dfadjliftmap 39525	. . 3 ⊢ ( I AdjLiftMap V) = (𝑚 ∈ dom (( I ∪ ◡ E ) ↾ V) ↦ [𝑚](( I ∪ ◡ E ) ↾ V))
4		dmresv 6197	. . . . 5 ⊢ dom (( I ∪ ◡ E ) ↾ V) = dom ( I ∪ ◡ E )
5		dmun 5893	. . . . . 6 ⊢ dom ( I ∪ ◡ E ) = (dom I ∪ dom ◡ E )
6		dmi 5904	. . . . . . 7 ⊢ dom I = V
7		dmcnvep 39457	. . . . . . 7 ⊢ dom ◡ E = (V ∖ {∅})
8	6, 7	uneq12i 4164	. . . . . 6 ⊢ (dom I ∪ dom ◡ E ) = (V ∪ (V ∖ {∅}))
9		undifabs 4433	. . . . . 6 ⊢ (V ∪ (V ∖ {∅})) = V
10	5, 8, 9	3eqtri 2787	. . . . 5 ⊢ dom ( I ∪ ◡ E ) = V
11	4, 10	eqtri 2783	. . . 4 ⊢ dom (( I ∪ ◡ E ) ↾ V) = V
12		orcom 884	. . . . . . 7 ⊢ ((𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚) ↔ (𝑛 ∈ 𝑚 ∨ 𝑛 ∈ {𝑚}))
13		elecALTV 39340	. . . . . . . . 9 ⊢ ((𝑚 ∈ V ∧ 𝑛 ∈ V) → (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑚( I ∪ ◡ E )𝑛))
14	13	el2v 3457	. . . . . . . 8 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑚( I ∪ ◡ E )𝑛)
15		brun 5155	. . . . . . . 8 ⊢ (𝑚( I ∪ ◡ E )𝑛 ↔ (𝑚 I 𝑛 ∨ 𝑚◡ E 𝑛))
16		equcom 2050	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 ↔ 𝑛 = 𝑚)
17		ideqg 5830	. . . . . . . . . . 11 ⊢ (𝑛 ∈ V → (𝑚 I 𝑛 ↔ 𝑚 = 𝑛))
18	17	elv 3455	. . . . . . . . . 10 ⊢ (𝑚 I 𝑛 ↔ 𝑚 = 𝑛)
19		velsn 4596	. . . . . . . . . 10 ⊢ (𝑛 ∈ {𝑚} ↔ 𝑛 = 𝑚)
20	16, 18, 19	3bitr4i 306	. . . . . . . . 9 ⊢ (𝑚 I 𝑛 ↔ 𝑛 ∈ {𝑚})
21		brcnvep 39339	. . . . . . . . . 10 ⊢ (𝑚 ∈ V → (𝑚◡ E 𝑛 ↔ 𝑛 ∈ 𝑚))
22	21	elv 3455	. . . . . . . . 9 ⊢ (𝑚◡ E 𝑛 ↔ 𝑛 ∈ 𝑚)
23	20, 22	orbi12i 928	. . . . . . . 8 ⊢ ((𝑚 I 𝑛 ∨ 𝑚◡ E 𝑛) ↔ (𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚))
24	14, 15, 23	3bitri 300	. . . . . . 7 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ (𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚))
25		elun 4151	. . . . . . 7 ⊢ (𝑛 ∈ (𝑚 ∪ {𝑚}) ↔ (𝑛 ∈ 𝑚 ∨ 𝑛 ∈ {𝑚}))
26	12, 24, 25	3bitr4i 306	. . . . . 6 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑛 ∈ (𝑚 ∪ {𝑚}))
27	26	eqriv 2757	. . . . 5 ⊢ [𝑚]( I ∪ ◡ E ) = (𝑚 ∪ {𝑚})
28		reli 5805	. . . . . . . 8 ⊢ Rel I
29		relcnv 6102	. . . . . . . 8 ⊢ Rel ◡ E
30		relun 5790	. . . . . . . 8 ⊢ (Rel ( I ∪ ◡ E ) ↔ (Rel I ∧ Rel ◡ E ))
31	28, 29, 30	mpbir2an 724	. . . . . . 7 ⊢ Rel ( I ∪ ◡ E )
32		dfrel3 6195	. . . . . . 7 ⊢ (Rel ( I ∪ ◡ E ) ↔ (( I ∪ ◡ E ) ↾ V) = ( I ∪ ◡ E ))
33	31, 32	mpbi 233	. . . . . 6 ⊢ (( I ∪ ◡ E ) ↾ V) = ( I ∪ ◡ E )
34	33	eceq2i 8768	. . . . 5 ⊢ [𝑚](( I ∪ ◡ E ) ↾ V) = [𝑚]( I ∪ ◡ E )
35		df-suc 6371	. . . . 5 ⊢ suc 𝑚 = (𝑚 ∪ {𝑚})
36	27, 34, 35	3eqtr4i 2793	. . . 4 ⊢ [𝑚](( I ∪ ◡ E ) ↾ V) = suc 𝑚
37	11, 36	mpteq12i 5201	. . 3 ⊢ (𝑚 ∈ dom (( I ∪ ◡ E ) ↾ V) ↦ [𝑚](( I ∪ ◡ E ) ↾ V)) = (𝑚 ∈ V ↦ suc 𝑚)
38		mptv 5210	. . 3 ⊢ (𝑚 ∈ V ↦ suc 𝑚) = {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚}
39	3, 37, 38	3eqtri 2787	. 2 ⊢ ( I AdjLiftMap V) = {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚}
40		df-sucmap 39531	. 2 ⊢ SucMap = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
41	2, 39, 40	3eqtr4ri 2794	1 ⊢ SucMap = ( I AdjLiftMap V)

This proof depends on syntax axioms:   ↔ wb 209   ∨ wo 861   = wceq 1569   ∈ wcel 2144  Vcvv 3450   ∖ cdif 4044   ∪ cun 4148  ∅c0 4277  {csn 4584   class class class wbr 5102  {copab 5166   ↦ cmpt 5185   I cid 5545   E cep 5550  ^◡ccnv 5650  dom cdm 5651   ↾ cres 5653  Rel wrel 5656  suc csuc 6367  [cec 8723   AdjLiftMap cadjliftmap 39245   SucMap csucmap 39247

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-12 2212  ax-ext 2732  ax-sep 5248  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5546  df-eprel 5551  df-xp 5657  df-rel 5658  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-suc 6371  df-ec 8727  df-qmap 39515  df-adjliftmap 39524  df-sucmap 39531

This theorem is used by:  dfsucmap2  39533