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	$$⊢2_{𝑜}{+}_{𝑜}{2}_{𝑜}=4_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		2on	$$⊢2_{𝑜}\in \mathrm{On}$$
2		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
3		oasuc	$$⊢\left(2_{𝑜}\in \mathrm{On}\wedge 1_{𝑜}\in \mathrm{On}\right)\to 2_{𝑜}{+}_{𝑜}\mathrm{suc}{1}_{𝑜}=\mathrm{suc}\left(2_{𝑜}{+}_{𝑜}{1}_{𝑜}\right)$$
4	1 2 3	mp2an	$$⊢2_{𝑜}{+}_{𝑜}\mathrm{suc}{1}_{𝑜}=\mathrm{suc}\left(2_{𝑜}{+}_{𝑜}{1}_{𝑜}\right)$$
5		df-2o	$$⊢2_{𝑜}=\mathrm{suc}{1}_{𝑜}$$
6	5	oveq2i	$$⊢2_{𝑜}{+}_{𝑜}{2}_{𝑜}=2_{𝑜}{+}_{𝑜}\mathrm{suc}{1}_{𝑜}$$
7		df-3o	$$⊢3_{𝑜}=\mathrm{suc}{2}_{𝑜}$$
8		oa1suc	$$⊢2_{𝑜}\in \mathrm{On}\to 2_{𝑜}{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}{2}_{𝑜}$$
9	1 8	ax-mp	$$⊢2_{𝑜}{+}_{𝑜}{1}_{𝑜}=\mathrm{suc}{2}_{𝑜}$$
10	7 9	eqtr4i	$$⊢3_{𝑜}=2_{𝑜}{+}_{𝑜}{1}_{𝑜}$$
11		suceq	$$⊢3_{𝑜}=2_{𝑜}{+}_{𝑜}{1}_{𝑜}\to \mathrm{suc}{3}_{𝑜}=\mathrm{suc}\left(2_{𝑜}{+}_{𝑜}{1}_{𝑜}\right)$$
12	10 11	ax-mp	$$⊢\mathrm{suc}{3}_{𝑜}=\mathrm{suc}\left(2_{𝑜}{+}_{𝑜}{1}_{𝑜}\right)$$
13	4 6 12	3eqtr4i	$$⊢2_{𝑜}{+}_{𝑜}{2}_{𝑜}=\mathrm{suc}{3}_{𝑜}$$
14		df-4o	$$⊢4_{𝑜}=\mathrm{suc}{3}_{𝑜}$$
15	13 14	eqtr4i	$$⊢2_{𝑜}{+}_{𝑜}{2}_{𝑜}=4_{𝑜}$$