Metamath Proof Explorer

Theorem o2p2e4OLD

Description: Obsolete version of o2p2e4 as of 23-Mar-2024. (Contributed by NM, 18-Aug-2021) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion o2p2e4OLD 
|- ( 2o +o 2o ) = 4o

Proof

Step Hyp Ref Expression
1 2on 
 |-  2o e. On
2 1on 
 |-  1o e. On
3 oasuc 
 |-  ( ( 2o e. On /\ 1o e. On ) -> ( 2o +o suc 1o ) = suc ( 2o +o 1o ) )
4 1 2 3 mp2an 
 |-  ( 2o +o suc 1o ) = suc ( 2o +o 1o )
5 df-2o 
 |-  2o = suc 1o
6 5 oveq2i 
 |-  ( 2o +o 2o ) = ( 2o +o suc 1o )
7 df-3o 
 |-  3o = suc 2o
8 oa1suc 
 |-  ( 2o e. On -> ( 2o +o 1o ) = suc 2o )
9 1 8 ax-mp 
 |-  ( 2o +o 1o ) = suc 2o
10 7 9 eqtr4i 
 |-  3o = ( 2o +o 1o )
11 suceq 
 |-  ( 3o = ( 2o +o 1o ) -> suc 3o = suc ( 2o +o 1o ) )
12 10 11 ax-mp 
 |-  suc 3o = suc ( 2o +o 1o )
13 4 6 12 3eqtr4i 
 |-  ( 2o +o 2o ) = suc 3o
14 df-4o 
 |-  4o = suc 3o
15 13 14 eqtr4i 
 |-  ( 2o +o 2o ) = 4o