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 Could not format assertion : No typesetting found for |- SucMap = ( _I AdjLiftMap _V ) with typecode |-

Proof

Step Hyp Ref Expression
1 eqcom ⊢ n = suc ⁡ m ↔ suc ⁡ m = n
2 1 opabbii ⊢ m n | n = suc ⁡ m = m n | suc ⁡ m = n
3 df-adjliftmap Could not format ( _I AdjLiftMap _V ) = ( m e. dom ( ( _I u. `' _E ) |` _V ) |-> [ m ] ( ( _I u. `' _E ) |` _V ) ) : No typesetting found for |- ( _I AdjLiftMap _V ) = ( m e. dom ( ( _I u. `' _E ) |` _V ) |-> [ m ] ( ( _I u. `' _E ) |` _V ) ) with typecode |-
4 dmresv ⊢ dom ⁡ I ∪ E -1 ↾ V = dom ⁡ I ∪ E -1
5 dmun ⊢ dom ⁡ I ∪ E -1 = dom ⁡ I ∪ dom ⁡ E -1
6 dmi ⊢ dom ⁡ I = V
7 dmcnvep ⊢ dom ⁡ E -1 = V ∖ ∅
8 6 7 uneq12i ⊢ dom ⁡ I ∪ dom ⁡ E -1 = V ∪ V ∖ ∅
9 undifabs ⊢ V ∪ V ∖ ∅ = V
10 5 8 9 3eqtri ⊢ dom ⁡ I ∪ E -1 = V
11 4 10 eqtri ⊢ dom ⁡ I ∪ E -1 ↾ V = V
12 orcom ⊢ n ∈ m ∨ n ∈ m ↔ n ∈ m ∨ n ∈ m
13 elecALTV ⊢ m ∈ V ∧ n ∈ V → n ∈ m I ∪ E -1 ↔ m I ∪ E -1 n
14 13 el2v ⊢ n ∈ m I ∪ E -1 ↔ m I ∪ E -1 n
15 brun ⊢ m I ∪ E -1 n ↔ m I n ∨ m E -1 n
16 equcom ⊢ m = n ↔ n = m
17 ideqg ⊢ n ∈ V → m I n ↔ m = n
18 17 elv ⊢ m I n ↔ m = n
19 velsn ⊢ n ∈ m ↔ n = m
20 16 18 19 3bitr4i ⊢ m I n ↔ n ∈ m
21 brcnvep ⊢ m ∈ V → m E -1 n ↔ n ∈ m
22 21 elv ⊢ m E -1 n ↔ n ∈ m
23 20 22 orbi12i ⊢ m I n ∨ m E -1 n ↔ n ∈ m ∨ n ∈ m
24 14 15 23 3bitri ⊢ n ∈ m I ∪ E -1 ↔ n ∈ m ∨ n ∈ m
25 elun ⊢ n ∈ m ∪ m ↔ n ∈ m ∨ n ∈ m
26 12 24 25 3bitr4i ⊢ n ∈ m I ∪ E -1 ↔ n ∈ m ∪ m
27 26 eqriv ⊢ m I ∪ E -1 = m ∪ m
28 reli ⊢ Rel ⁡ I
29 relcnv ⊢ Rel ⁡ E -1
30 relun ⊢ Rel ⁡ I ∪ E -1 ↔ Rel ⁡ I ∧ Rel ⁡ E -1
31 28 29 30 mpbir2an ⊢ Rel ⁡ I ∪ E -1
32 dfrel3 ⊢ Rel ⁡ I ∪ E -1 ↔ I ∪ E -1 ↾ V = I ∪ E -1
33 31 32 mpbi ⊢ I ∪ E -1 ↾ V = I ∪ E -1
34 33 eceq2i ⊢ m I ∪ E -1 ↾ V = m I ∪ E -1
35 df-suc ⊢ suc ⁡ m = m ∪ m
36 27 34 35 3eqtr4i ⊢ m I ∪ E -1 ↾ V = suc ⁡ m
37 11 36 mpteq12i ⊢ m ∈ dom ⁡ I ∪ E -1 ↾ V ⟼ m I ∪ E -1 ↾ V = m ∈ V ⟼ suc ⁡ m
38 mptv ⊢ m ∈ V ⟼ suc ⁡ m = m n | n = suc ⁡ m
39 3 37 38 3eqtri Could not format ( _I AdjLiftMap _V ) = { <. m , n >. | n = suc m } : No typesetting found for |- ( _I AdjLiftMap _V ) = { <. m , n >. | n = suc m } with typecode |-
40 df-sucmap Could not format SucMap = { <. m , n >. | suc m = n } : No typesetting found for |- SucMap = { <. m , n >. | suc m = n } with typecode |-
41 2 39 40 3eqtr4ri Could not format SucMap = ( _I AdjLiftMap _V ) : No typesetting found for |- SucMap = ( _I AdjLiftMap _V ) with typecode |-