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 On$
2		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
3		peano1	$⊢ \emptyset \in ω$
4		peano2	$⊢ \emptyset \in ω \to suc \emptyset \in ω$
5	3 4	ax-mp	$⊢ suc \emptyset \in ω$
6	2 5	eqeltri	$⊢ 1_{𝑜} \in ω$
7		onasuc	$⊢ (2_{𝑜} \in On \land 1_{𝑜} \in ω) \to 2_{𝑜} +_{𝑜} suc 1_{𝑜} = suc (2_{𝑜} +_{𝑜} 1_{𝑜})$
8	1 6 7	mp2an	$⊢ 2_{𝑜} +_{𝑜} suc 1_{𝑜} = suc (2_{𝑜} +_{𝑜} 1_{𝑜})$
9		df-2o	$⊢ 2_{𝑜} = suc 1_{𝑜}$
10	9	oveq2i	$⊢ 2_{𝑜} +_{𝑜} 2_{𝑜} = 2_{𝑜} +_{𝑜} suc 1_{𝑜}$
11		df-3o	$⊢ 3_{𝑜} = suc 2_{𝑜}$
12		oa1suc	$⊢ 2_{𝑜} \in On \to 2_{𝑜} +_{𝑜} 1_{𝑜} = suc 2_{𝑜}$
13	1 12	ax-mp	$⊢ 2_{𝑜} +_{𝑜} 1_{𝑜} = suc 2_{𝑜}$
14	11 13	eqtr4i	$⊢ 3_{𝑜} = 2_{𝑜} +_{𝑜} 1_{𝑜}$
15		suceq	$⊢ 3_{𝑜} = 2_{𝑜} +_{𝑜} 1_{𝑜} \to suc 3_{𝑜} = suc (2_{𝑜} +_{𝑜} 1_{𝑜})$
16	14 15	ax-mp	$⊢ suc 3_{𝑜} = suc (2_{𝑜} +_{𝑜} 1_{𝑜})$
17	8 10 16	3eqtr4i	$⊢ 2_{𝑜} +_{𝑜} 2_{𝑜} = suc 3_{𝑜}$
18		df-4o	$⊢ 4_{𝑜} = suc 3_{𝑜}$
19	17 18	eqtr4i	$⊢ 2_{𝑜} +_{𝑜} 2_{𝑜} = 4_{𝑜}$

Metamath Proof Explorer

Theorem o2p2e4

Proof