Theorem xp2dju

Description: Two times a cardinal number. Exercise 4.56(g) of Mendelson p. 258. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	xp2dju	$$⊢2_{𝑜}\times A=\left(A\mathrm{\bigsqcup ︀}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xpundir	$$⊢\left(\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}\right)\times A=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times A\right)$$
2		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
3		df-pr	$$⊢\left\{\varnothing ,1_{𝑜}\right\}=\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}$$
4	2 3	eqtri	$$⊢2_{𝑜}=\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}$$
5	4	xpeq1i	$$⊢2_{𝑜}\times A=\left(\left\{\varnothing \right\}\cup \left\{1_{𝑜}\right\}\right)\times A$$
6		df-dju	$$⊢\left(A\mathrm{\bigsqcup ︀}A\right)=\left(\left\{\varnothing \right\}\times A\right)\cup \left(\left\{1_{𝑜}\right\}\times A\right)$$
7	1 5 6	3eqtr4i	$$⊢2_{𝑜}\times A=\left(A\mathrm{\bigsqcup ︀}A\right)$$