Theorem djucomen

Description: Commutative law for cardinal addition. Exercise 4.56(c) of Mendelson p. 258. (Contributed by NM, 24-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	djucomen	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\approx \left(B\mathrm{\bigsqcup ︀}A\right)$$

Proof

Step	Hyp	Ref	Expression
1		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
2		xpsnen2g	$$⊢\left(1_{𝑜}\in \mathrm{V}\wedge A\in V\right)\to \left(\left\{1_{𝑜}\right\}\times A\right)\approx A$$
3	1 2	mpan	$$⊢A\in V\to \left(\left\{1_{𝑜}\right\}\times A\right)\approx A$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5		xpsnen2g	$$⊢\left(\varnothing \in \mathrm{V}\wedge B\in W\right)\to \left(\left\{\varnothing \right\}\times B\right)\approx B$$
6	4 5	mpan	$$⊢B\in W\to \left(\left\{\varnothing \right\}\times B\right)\approx B$$
7		ensym	$$⊢\left(\left\{1_{𝑜}\right\}\times A\right)\approx A\to A\approx \left(\left\{1_{𝑜}\right\}\times A\right)$$
8		ensym	$$⊢\left(\left\{\varnothing \right\}\times B\right)\approx B\to B\approx \left(\left\{\varnothing \right\}\times B\right)$$
9		incom	$$⊢\left(\left\{1_{𝑜}\right\}\times A\right)\cap \left(\left\{\varnothing \right\}\times B\right)=\left(\left\{\varnothing \right\}\times B\right)\cap \left(\left\{1_{𝑜}\right\}\times A\right)$$
10		xp01disjl	$$⊢\left(\left\{\varnothing \right\}\times B\right)\cap \left(\left\{1_{𝑜}\right\}\times A\right)=\varnothing$$
11	9 10	eqtri	$$⊢\left(\left\{1_{𝑜}\right\}\times A\right)\cap \left(\left\{\varnothing \right\}\times B\right)=\varnothing$$
12		djuenun	$$⊢\left(A\approx \left(\left\{1_{𝑜}\right\}\times A\right)\wedge B\approx \left(\left\{\varnothing \right\}\times B\right)\wedge \left(\left\{1_{𝑜}\right\}\times A\right)\cap \left(\left\{\varnothing \right\}\times B\right)=\varnothing \right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\approx \left(\left(\left\{1_{𝑜}\right\}\times A\right)\cup \left(\left\{\varnothing \right\}\times B\right)\right)$$
13	11 12	mp3an3	$$⊢\left(A\approx \left(\left\{1_{𝑜}\right\}\times A\right)\wedge B\approx \left(\left\{\varnothing \right\}\times B\right)\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\approx \left(\left(\left\{1_{𝑜}\right\}\times A\right)\cup \left(\left\{\varnothing \right\}\times B\right)\right)$$
14	7 8 13	syl2an	$$⊢\left(\left(\left\{1_{𝑜}\right\}\times A\right)\approx A\wedge \left(\left\{\varnothing \right\}\times B\right)\approx B\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\approx \left(\left(\left\{1_{𝑜}\right\}\times A\right)\cup \left(\left\{\varnothing \right\}\times B\right)\right)$$
15	3 6 14	syl2an	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\approx \left(\left(\left\{1_{𝑜}\right\}\times A\right)\cup \left(\left\{\varnothing \right\}\times B\right)\right)$$
16		df-dju	$$⊢\left(B\mathrm{\bigsqcup ︀}A\right)=\left(\left\{\varnothing \right\}\times B\right)\cup \left(\left\{1_{𝑜}\right\}\times A\right)$$
17	16	equncomi	$$⊢\left(B\mathrm{\bigsqcup ︀}A\right)=\left(\left\{1_{𝑜}\right\}\times A\right)\cup \left(\left\{\varnothing \right\}\times B\right)$$
18	15 17	breqtrrdi	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\mathrm{\bigsqcup ︀}B\right)\approx \left(B\mathrm{\bigsqcup ︀}A\right)$$