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 ∈ On
2		1on	⊢ 1o ∈ On
3		oasuc	⊢ ( ( 2o ∈ On ∧ 1o ∈ 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 ∈ 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