Metamath Proof Explorer

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	$⊢ (A \in V \land B \in W) \to (A ⊔︀ B) \approx (B ⊔︀ A)$

Proof

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