This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem oa1suc

Description: Addition with 1 is same as successor. Proposition 4.34(a) of Mendelson p. 266. Remark 2.4 of Schloeder p. 4. (Contributed by NM, 29-Oct-1995) (Revised by Mario Carneiro, 16-Nov-2014)

		Ref	Expression
	Assertion	oa1suc	$⊢ A \in On \to A +_{𝑜} 1_{𝑜} = suc A$

Proof

Step	Hyp	Ref	Expression
1		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
2	1	oveq2i	$⊢ A +_{𝑜} 1_{𝑜} = A +_{𝑜} suc \emptyset$
3		peano1	$⊢ \emptyset \in ω$
4		onasuc	$⊢ (A \in On \land \emptyset \in ω) \to A +_{𝑜} suc \emptyset = suc (A +_{𝑜} \emptyset)$
5	3 4	mpan2	$⊢ A \in On \to A +_{𝑜} suc \emptyset = suc (A +_{𝑜} \emptyset)$
6	2 5	eqtrid	$⊢ A \in On \to A +_{𝑜} 1_{𝑜} = suc (A +_{𝑜} \emptyset)$
7		oa0	$⊢ A \in On \to A +_{𝑜} \emptyset = A$
8		suceq	$⊢ A +_{𝑜} \emptyset = A \to suc (A +_{𝑜} \emptyset) = suc A$
9	7 8	syl	$⊢ A \in On \to suc (A +_{𝑜} \emptyset) = suc A$
10	6 9	eqtrd	$⊢ A \in On \to A +_{𝑜} 1_{𝑜} = suc A$