This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 df-adjliftmap ⊢ ( 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 )