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 ∈ 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