Theorem dfsucmap3 38962

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 2769	. . 3 ⊢ (𝑛 = suc 𝑚 ↔ suc 𝑚 = 𝑛)
2	1	opabbii 5167	. 2 ⊢ {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚} = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
3		dfadjliftmap 38955	. . 3 ⊢ ( I AdjLiftMap V) = (𝑚 ∈ dom (( I ∪ ◡ E ) ↾ V) ↦ [𝑚](( I ∪ ◡ E ) ↾ V))
4		dmresv 6187	. . . . 5 ⊢ dom (( I ∪ ◡ E ) ↾ V) = dom ( I ∪ ◡ E )
5		dmun 5886	. . . . . 6 ⊢ dom ( I ∪ ◡ E ) = (dom I ∪ dom ◡ E )
6		dmi 5897	. . . . . . 7 ⊢ dom I = V
7		dmcnvep 38887	. . . . . . 7 ⊢ dom ◡ E = (V ∖ {∅})
8	6, 7	uneq12i 4119	. . . . . 6 ⊢ (dom I ∪ dom ◡ E ) = (V ∪ (V ∖ {∅}))
9		undifabs 4432	. . . . . 6 ⊢ (V ∪ (V ∖ {∅})) = V
10	5, 8, 9	3eqtri 2789	. . . . 5 ⊢ dom ( I ∪ ◡ E ) = V
11	4, 10	eqtri 2785	. . . 4 ⊢ dom (( I ∪ ◡ E ) ↾ V) = V
12		orcom 881	. . . . . . 7 ⊢ ((𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚) ↔ (𝑛 ∈ 𝑚 ∨ 𝑛 ∈ {𝑚}))
13		elecALTV 38770	. . . . . . . . 9 ⊢ ((𝑚 ∈ V ∧ 𝑛 ∈ V) → (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑚( I ∪ ◡ E )𝑛))
14	13	el2v 3461	. . . . . . . 8 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑚( I ∪ ◡ E )𝑛)
15		brun 5151	. . . . . . . 8 ⊢ (𝑚( I ∪ ◡ E )𝑛 ↔ (𝑚 I 𝑛 ∨ 𝑚◡ E 𝑛))
16		equcom 2038	. . . . . . . . . 10 ⊢ (𝑚 = 𝑛 ↔ 𝑛 = 𝑚)
17		ideqg 5823	. . . . . . . . . . 11 ⊢ (𝑛 ∈ V → (𝑚 I 𝑛 ↔ 𝑚 = 𝑛))
18	17	elv 3459	. . . . . . . . . 10 ⊢ (𝑚 I 𝑛 ↔ 𝑚 = 𝑛)
19		velsn 4598	. . . . . . . . . 10 ⊢ (𝑛 ∈ {𝑚} ↔ 𝑛 = 𝑚)
20	16, 18, 19	3bitr4i 305	. . . . . . . . 9 ⊢ (𝑚 I 𝑛 ↔ 𝑛 ∈ {𝑚})
21		brcnvep 38769	. . . . . . . . . 10 ⊢ (𝑚 ∈ V → (𝑚◡ E 𝑛 ↔ 𝑛 ∈ 𝑚))
22	21	elv 3459	. . . . . . . . 9 ⊢ (𝑚◡ E 𝑛 ↔ 𝑛 ∈ 𝑚)
23	20, 22	orbi12i 925	. . . . . . . 8 ⊢ ((𝑚 I 𝑛 ∨ 𝑚◡ E 𝑛) ↔ (𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚))
24	14, 15, 23	3bitri 299	. . . . . . 7 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ (𝑛 ∈ {𝑚} ∨ 𝑛 ∈ 𝑚))
25		elun 4106	. . . . . . 7 ⊢ (𝑛 ∈ (𝑚 ∪ {𝑚}) ↔ (𝑛 ∈ 𝑚 ∨ 𝑛 ∈ {𝑚}))
26	12, 24, 25	3bitr4i 305	. . . . . 6 ⊢ (𝑛 ∈ [𝑚]( I ∪ ◡ E ) ↔ 𝑛 ∈ (𝑚 ∪ {𝑚}))
27	26	eqriv 2759	. . . . 5 ⊢ [𝑚]( I ∪ ◡ E ) = (𝑚 ∪ {𝑚})
28		reli 5799	. . . . . . . 8 ⊢ Rel I
29		relcnv 6093	. . . . . . . 8 ⊢ Rel ◡ E
30		relun 5784	. . . . . . . 8 ⊢ (Rel ( I ∪ ◡ E ) ↔ (Rel I ∧ Rel ◡ E ))
31	28, 29, 30	mpbir2an 721	. . . . . . 7 ⊢ Rel ( I ∪ ◡ E )
32		dfrel3 6185	. . . . . . 7 ⊢ (Rel ( I ∪ ◡ E ) ↔ (( I ∪ ◡ E ) ↾ V) = ( I ∪ ◡ E ))
33	31, 32	mpbi 232	. . . . . 6 ⊢ (( I ∪ ◡ E ) ↾ V) = ( I ∪ ◡ E )
34	33	eceq2i 8721	. . . . 5 ⊢ [𝑚](( I ∪ ◡ E ) ↾ V) = [𝑚]( I ∪ ◡ E )
35		df-suc 6352	. . . . 5 ⊢ suc 𝑚 = (𝑚 ∪ {𝑚})
36	27, 34, 35	3eqtr4i 2795	. . . 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 2789	. 2 ⊢ ( I AdjLiftMap V) = {⟨𝑚, 𝑛⟩ ∣ 𝑛 = suc 𝑚}
40		df-sucmap 38961	. 2 ⊢ SucMap = {⟨𝑚, 𝑛⟩ ∣ suc 𝑚 = 𝑛}
41	2, 39, 40	3eqtr4ri 2796	1 ⊢ SucMap = ( I AdjLiftMap V)

Syntax hints:   ↔ wb 208   ∨ wo 858   = wceq 1560   ∈ wcel 2142  Vcvv 3454   ∖ cdif 3901   ∪ cun 3902  ∅c0 4285  {csn 4582   class class class wbr 5100  {copab 5162   ↦ cmpt 5181   I cid 5541   E cep 5546  ^◡ccnv 5646  dom cdm 5647   ↾ cres 5649  Rel wrel 5652  suc csuc 6348  [cec 8676   AdjLiftMap cadjliftmap 38675   SucMap csucmap 38677

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-10 2175  ax-12 2212  ax-ext 2734  ax-sep 5246  ax-pr 5390

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-nf 1804  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rex 3087  df-rab 3415  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-mpt 5182  df-id 5542  df-eprel 5547  df-xp 5653  df-rel 5654  df-cnv 5655  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-suc 6352  df-ec 8680  df-qmap 38945  df-adjliftmap 38954  df-sucmap 38961

This theorem is referenced by:  dfsucmap2  38963