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

Proof

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