Theorem oa0

Description: Addition with zero. Proposition 8.3 of TakeutiZaring p. 57. (Contributed by NM, 3-May-1995) (Revised by Mario Carneiro, 8-Sep-2013)

	Ref	Expression
Assertion	oa0	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}\varnothing =A$$

Proof

Step	Hyp	Ref	Expression
1		0elon	$$⊢\varnothing \in \mathrm{On}$$
2		oav	$$⊢\left(A\in \mathrm{On}\wedge \varnothing \in \mathrm{On}\right)\to A{+}_{𝑜}\varnothing =\mathrm{rec}\left(\left(x\in \mathrm{V}⟼\mathrm{suc}x\right),A\right)\left(\varnothing \right)$$
3	1 2	mpan2	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}\varnothing =\mathrm{rec}\left(\left(x\in \mathrm{V}⟼\mathrm{suc}x\right),A\right)\left(\varnothing \right)$$
4		rdg0g	$$⊢A\in \mathrm{On}\to \mathrm{rec}\left(\left(x\in \mathrm{V}⟼\mathrm{suc}x\right),A\right)\left(\varnothing \right)=A$$
5	3 4	eqtrd	$$⊢A\in \mathrm{On}\to A{+}_{𝑜}\varnothing =A$$