This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Union Ordinal arithmetic 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 ∈ On
2
df-1o ⊢ 1o = suc ∅
3
peano1 ⊢ ∅ ∈ ω
4
peano2 ⊢ ( ∅ ∈ ω → suc ∅ ∈ ω )
5
3 4
ax-mp ⊢ suc ∅ ∈ ω
6
2 5
eqeltri ⊢ 1o ∈ ω
7
onasuc ⊢ ( ( 2o ∈ On ∧ 1o ∈ ω ) → ( 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 ∈ 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