Theorem dfsucmap3

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

	Ref	Expression
Assertion	dfsucmap3	⊢ SucMap = ( I AdjLiftMap V )

Proof

Step	Hyp	Ref	Expression
1		eqcom	⊢ ( 𝑛 = suc 𝑚 ↔ suc 𝑚 = 𝑛 )
2	1	opabbii	⊢ { ⟨ 𝑚 , 𝑛 ⟩ ∣ 𝑛 = suc 𝑚 } = { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }
3		dfadjliftmap	⊢ ( I AdjLiftMap V ) = ( 𝑚 ∈ dom ( ( I ∪ ◡ E ) ↾ V ) ↦ [ 𝑚 ] ( ( I ∪ ◡ E ) ↾ V ) )
4		dmresv	⊢ dom ( ( I ∪ ◡ E ) ↾ V ) = dom ( I ∪ ◡ E )
5		dmun	⊢ dom ( I ∪ ◡ E ) = ( dom I ∪ dom ◡ E )
6		dmi	⊢ dom I = V
7		dmcnvep	⊢ dom ◡ E = ( V ∖ { ∅ } )
8	6 7	uneq12i	⊢ ( dom I ∪ dom ◡ E ) = ( V ∪ ( V ∖ { ∅ } ) )
9		undifabs	⊢ ( V ∪ ( V ∖ { ∅ } ) ) = V
10	5 8 9	3eqtri	⊢ dom ( I ∪ ◡ E ) = V
11	4 10	eqtri	⊢ dom ( ( I ∪ ◡ E ) ↾ V ) = V
12		orcom	⊢ ( ( 𝑛 ∈ { 𝑚 } ∨ 𝑛 ∈ 𝑚 ) ↔ ( 𝑛 ∈ 𝑚 ∨ 𝑛 ∈ { 𝑚 } ) )
13		elecALTV	⊢ ( ( 𝑚 ∈ V ∧ 𝑛 ∈ V ) → ( 𝑛 ∈ [ 𝑚 ] ( I ∪ ◡ E ) ↔ 𝑚 ( I ∪ ◡ E ) 𝑛 ) )
14	13	el2v	⊢ ( 𝑛 ∈ [ 𝑚 ] ( I ∪ ◡ E ) ↔ 𝑚 ( I ∪ ◡ E ) 𝑛 )
15		brun	⊢ ( 𝑚 ( I ∪ ◡ E ) 𝑛 ↔ ( 𝑚 I 𝑛 ∨ 𝑚 ◡ E 𝑛 ) )
16		equcom	⊢ ( 𝑚 = 𝑛 ↔ 𝑛 = 𝑚 )
17		ideqg	⊢ ( 𝑛 ∈ V → ( 𝑚 I 𝑛 ↔ 𝑚 = 𝑛 ) )
18	17	elv	⊢ ( 𝑚 I 𝑛 ↔ 𝑚 = 𝑛 )
19		velsn	⊢ ( 𝑛 ∈ { 𝑚 } ↔ 𝑛 = 𝑚 )
20	16 18 19	3bitr4i	⊢ ( 𝑚 I 𝑛 ↔ 𝑛 ∈ { 𝑚 } )
21		brcnvep	⊢ ( 𝑚 ∈ V → ( 𝑚 ◡ E 𝑛 ↔ 𝑛 ∈ 𝑚 ) )
22	21	elv	⊢ ( 𝑚 ◡ E 𝑛 ↔ 𝑛 ∈ 𝑚 )
23	20 22	orbi12i	⊢ ( ( 𝑚 I 𝑛 ∨ 𝑚 ◡ E 𝑛 ) ↔ ( 𝑛 ∈ { 𝑚 } ∨ 𝑛 ∈ 𝑚 ) )
24	14 15 23	3bitri	⊢ ( 𝑛 ∈ [ 𝑚 ] ( I ∪ ◡ E ) ↔ ( 𝑛 ∈ { 𝑚 } ∨ 𝑛 ∈ 𝑚 ) )
25		elun	⊢ ( 𝑛 ∈ ( 𝑚 ∪ { 𝑚 } ) ↔ ( 𝑛 ∈ 𝑚 ∨ 𝑛 ∈ { 𝑚 } ) )
26	12 24 25	3bitr4i	⊢ ( 𝑛 ∈ [ 𝑚 ] ( I ∪ ◡ E ) ↔ 𝑛 ∈ ( 𝑚 ∪ { 𝑚 } ) )
27	26	eqriv	⊢ [ 𝑚 ] ( I ∪ ◡ E ) = ( 𝑚 ∪ { 𝑚 } )
28		reli	⊢ Rel I
29		relcnv	⊢ Rel ◡ E
30		relun	⊢ ( Rel ( I ∪ ◡ E ) ↔ ( Rel I ∧ Rel ◡ E ) )
31	28 29 30	mpbir2an	⊢ Rel ( I ∪ ◡ E )
32		dfrel3	⊢ ( Rel ( I ∪ ◡ E ) ↔ ( ( I ∪ ◡ E ) ↾ V ) = ( I ∪ ◡ E ) )
33	31 32	mpbi	⊢ ( ( I ∪ ◡ E ) ↾ V ) = ( I ∪ ◡ E )
34	33	eceq2i	⊢ [ 𝑚 ] ( ( I ∪ ◡ E ) ↾ V ) = [ 𝑚 ] ( I ∪ ◡ E )
35		df-suc	⊢ suc 𝑚 = ( 𝑚 ∪ { 𝑚 } )
36	27 34 35	3eqtr4i	⊢ [ 𝑚 ] ( ( I ∪ ◡ E ) ↾ V ) = suc 𝑚
37	11 36	mpteq12i	⊢ ( 𝑚 ∈ dom ( ( I ∪ ◡ E ) ↾ V ) ↦ [ 𝑚 ] ( ( I ∪ ◡ E ) ↾ V ) ) = ( 𝑚 ∈ V ↦ suc 𝑚 )
38		mptv	⊢ ( 𝑚 ∈ V ↦ suc 𝑚 ) = { ⟨ 𝑚 , 𝑛 ⟩ ∣ 𝑛 = suc 𝑚 }
39	3 37 38	3eqtri	⊢ ( I AdjLiftMap V ) = { ⟨ 𝑚 , 𝑛 ⟩ ∣ 𝑛 = suc 𝑚 }
40		df-sucmap	⊢ SucMap = { ⟨ 𝑚 , 𝑛 ⟩ ∣ suc 𝑚 = 𝑛 }
41	2 39 40	3eqtr4ri	⊢ SucMap = ( I AdjLiftMap V )