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

Metamath Proof Explorer

Theorem o2p2e4

Description: 2 + 2 = 4 for ordinal numbers. Ordinal numbers are modeled as Von Neumann ordinals; see df-suc . For the usual proof using complex numbers, see 2p2e4 . (Contributed by NM, 18-Aug-2021) Avoid ax-rep , from a comment by Sophie. (Revised by SN, 23-Mar-2024)

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

Proof

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