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 
 |-  ( n = suc m <-> suc m = n )
2 1 opabbii 
 |-  { <. m , n >. | n = suc m } = { <. m , n >. | suc m = n }
3 df-adjliftmap 
 |-  ( _I AdjLiftMap _V ) = ( m e. dom ( ( _I u. `' _E ) |` _V ) |-> [ m ] ( ( _I u. `' _E ) |` _V ) )
4 dmresv 
 |-  dom ( ( _I u. `' _E ) |` _V ) = dom ( _I u. `' _E )
5 dmun 
 |-  dom ( _I u. `' _E ) = ( dom _I u. dom `' _E )
6 dmi 
 |-  dom _I = _V
7 dmcnvep 
 |-  dom `' _E = ( _V \ { (/) } )
8 6 7 uneq12i 
 |-  ( dom _I u. dom `' _E ) = ( _V u. ( _V \ { (/) } ) )
9 undifabs 
 |-  ( _V u. ( _V \ { (/) } ) ) = _V
10 5 8 9 3eqtri 
 |-  dom ( _I u. `' _E ) = _V
11 4 10 eqtri 
 |-  dom ( ( _I u. `' _E ) |` _V ) = _V
12 orcom 
 |-  ( ( n e. { m } \/ n e. m ) <-> ( n e. m \/ n e. { m } ) )
13 elecALTV 
 |-  ( ( m e. _V /\ n e. _V ) -> ( n e. [ m ] ( _I u. `' _E ) <-> m ( _I u. `' _E ) n ) )
14 13 el2v 
 |-  ( n e. [ m ] ( _I u. `' _E ) <-> m ( _I u. `' _E ) n )
15 brun 
 |-  ( m ( _I u. `' _E ) n <-> ( m _I n \/ m `' _E n ) )
16 equcom 
 |-  ( m = n <-> n = m )
17 ideqg 
 |-  ( n e. _V -> ( m _I n <-> m = n ) )
18 17 elv 
 |-  ( m _I n <-> m = n )
19 velsn 
 |-  ( n e. { m } <-> n = m )
20 16 18 19 3bitr4i 
 |-  ( m _I n <-> n e. { m } )
21 brcnvep 
 |-  ( m e. _V -> ( m `' _E n <-> n e. m ) )
22 21 elv 
 |-  ( m `' _E n <-> n e. m )
23 20 22 orbi12i 
 |-  ( ( m _I n \/ m `' _E n ) <-> ( n e. { m } \/ n e. m ) )
24 14 15 23 3bitri 
 |-  ( n e. [ m ] ( _I u. `' _E ) <-> ( n e. { m } \/ n e. m ) )
25 elun 
 |-  ( n e. ( m u. { m } ) <-> ( n e. m \/ n e. { m } ) )
26 12 24 25 3bitr4i 
 |-  ( n e. [ m ] ( _I u. `' _E ) <-> n e. ( m u. { m } ) )
27 26 eqriv 
 |-  [ m ] ( _I u. `' _E ) = ( m u. { m } )
28 reli 
 |-  Rel _I
29 relcnv 
 |-  Rel `' _E
30 relun 
 |-  ( Rel ( _I u. `' _E ) <-> ( Rel _I /\ Rel `' _E ) )
31 28 29 30 mpbir2an 
 |-  Rel ( _I u. `' _E )
32 dfrel3 
 |-  ( Rel ( _I u. `' _E ) <-> ( ( _I u. `' _E ) |` _V ) = ( _I u. `' _E ) )
33 31 32 mpbi 
 |-  ( ( _I u. `' _E ) |` _V ) = ( _I u. `' _E )
34 33 eceq2i 
 |-  [ m ] ( ( _I u. `' _E ) |` _V ) = [ m ] ( _I u. `' _E )
35 df-suc 
 |-  suc m = ( m u. { m } )
36 27 34 35 3eqtr4i 
 |-  [ m ] ( ( _I u. `' _E ) |` _V ) = suc m
37 11 36 mpteq12i 
 |-  ( m e. dom ( ( _I u. `' _E ) |` _V ) |-> [ m ] ( ( _I u. `' _E ) |` _V ) ) = ( m e. _V |-> suc m )
38 mptv 
 |-  ( m e. _V |-> suc m ) = { <. m , n >. | n = suc m }
39 3 37 38 3eqtri 
 |-  ( _I AdjLiftMap _V ) = { <. m , n >. | n = suc m }
40 df-sucmap 
 |-  SucMap = { <. m , n >. | suc m = n }
41 2 39 40 3eqtr4ri 
 |-  SucMap = ( _I AdjLiftMap _V )