djuassen

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

		Ref	Expression
	Assertion	djuassen	$⊢ (A \in V \land B \in W \land C \in X) \to ((A ⊔︀ B) ⊔︀ C) \approx (A ⊔︀ (B ⊔︀ C))$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		simp1	$⊢ (A \in V \land B \in W \land C \in X) \to A \in V$
3		xpsnen2g	$⊢ (\emptyset \in V \land A \in V) \to (\{\emptyset\} \times A) \approx A$
4	1 2 3	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to (\{\emptyset\} \times A) \approx A$
5	4	ensymd	$⊢ (A \in V \land B \in W \land C \in X) \to A \approx (\{\emptyset\} \times A)$
6		1oex	$⊢ 1_{𝑜} \in V$
7		snex	$⊢ \{\emptyset\} \in V$
8		simp2	$⊢ (A \in V \land B \in W \land C \in X) \to B \in W$
9		xpexg	$⊢ (\{\emptyset\} \in V \land B \in W) \to \{\emptyset\} \times B \in V$
10	7 8 9	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to \{\emptyset\} \times B \in V$
11		xpsnen2g	$⊢ (1_{𝑜} \in V \land \{\emptyset\} \times B \in V) \to (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \approx (\{\emptyset\} \times B)$
12	6 10 11	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \approx (\{\emptyset\} \times B)$
13		xpsnen2g	$⊢ (\emptyset \in V \land B \in W) \to (\{\emptyset\} \times B) \approx B$
14	1 8 13	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to (\{\emptyset\} \times B) \approx B$
15		entr	$⊢ ((\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \approx (\{\emptyset\} \times B) \land (\{\emptyset\} \times B) \approx B) \to (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \approx B$
16	12 14 15	syl2anc	$⊢ (A \in V \land B \in W \land C \in X) \to (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \approx B$
17	16	ensymd	$⊢ (A \in V \land B \in W \land C \in X) \to B \approx (\{1_{𝑜}\} \times (\{\emptyset\} \times B))$
18		xp01disjl	$⊢ (\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) = \emptyset$
19	18	a1i	$⊢ (A \in V \land B \in W \land C \in X) \to (\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) = \emptyset$
20		djuenun	$⊢ (A \approx (\{\emptyset\} \times A) \land B \approx (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \land (\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) = \emptyset) \to (A ⊔︀ B) \approx ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (\{\emptyset\} \times B)))$
21	5 17 19 20	syl3anc	$⊢ (A \in V \land B \in W \land C \in X) \to (A ⊔︀ B) \approx ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (\{\emptyset\} \times B)))$
22		snex	$⊢ \{1_{𝑜}\} \in V$
23		simp3	$⊢ (A \in V \land B \in W \land C \in X) \to C \in X$
24		xpexg	$⊢ (\{1_{𝑜}\} \in V \land C \in X) \to \{1_{𝑜}\} \times C \in V$
25	22 23 24	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to \{1_{𝑜}\} \times C \in V$
26		xpsnen2g	$⊢ (1_{𝑜} \in V \land \{1_{𝑜}\} \times C \in V) \to (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) \approx (\{1_{𝑜}\} \times C)$
27	6 25 26	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) \approx (\{1_{𝑜}\} \times C)$
28		xpsnen2g	$⊢ (1_{𝑜} \in V \land C \in X) \to (\{1_{𝑜}\} \times C) \approx C$
29	6 23 28	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to (\{1_{𝑜}\} \times C) \approx C$
30		entr	$⊢ ((\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) \approx (\{1_{𝑜}\} \times C) \land (\{1_{𝑜}\} \times C) \approx C) \to (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) \approx C$
31	27 29 30	syl2anc	$⊢ (A \in V \land B \in W \land C \in X) \to (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) \approx C$
32	31	ensymd	$⊢ (A \in V \land B \in W \land C \in X) \to C \approx (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C))$
33		indir	$⊢ ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (\{\emptyset\} \times B))) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) = ((\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C))) \cup ((\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)))$
34		xp01disjl	$⊢ (\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) = \emptyset$
35		xp01disjl	$⊢ (\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times C) = \emptyset$
36	35	xpeq2i	$⊢ \{1_{𝑜}\} \times ((\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times C)) = \{1_{𝑜}\} \times \emptyset$
37		xpindi	$⊢ \{1_{𝑜}\} \times ((\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times C)) = (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C))$
38		xp0	$⊢ \{1_{𝑜}\} \times \emptyset = \emptyset$
39	36 37 38	3eqtr3i	$⊢ (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) = \emptyset$
40	34 39	uneq12i	$⊢ ((\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C))) \cup ((\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C))) = \emptyset \cup \emptyset$
41		un0	$⊢ \emptyset \cup \emptyset = \emptyset$
42	40 41	eqtri	$⊢ ((\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C))) \cup ((\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C))) = \emptyset$
43	33 42	eqtri	$⊢ ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (\{\emptyset\} \times B))) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) = \emptyset$
44	43	a1i	$⊢ (A \in V \land B \in W \land C \in X) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (\{\emptyset\} \times B))) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) = \emptyset$
45		djuenun	$⊢ ((A ⊔︀ B) \approx ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (\{\emptyset\} \times B))) \land C \approx (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) \land ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (\{\emptyset\} \times B))) \cap (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) = \emptyset) \to ((A ⊔︀ B) ⊔︀ C) \approx (((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (\{\emptyset\} \times B))) \cup (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)))$
46	21 32 44 45	syl3anc	$⊢ (A \in V \land B \in W \land C \in X) \to ((A ⊔︀ B) ⊔︀ C) \approx (((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (\{\emptyset\} \times B))) \cup (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)))$
47		df-dju	$⊢ (B ⊔︀ C) = (\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C)$
48	47	xpeq2i	$⊢ \{1_{𝑜}\} \times (B ⊔︀ C) = \{1_{𝑜}\} \times ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C))$
49		xpundi	$⊢ \{1_{𝑜}\} \times ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C)) = (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \cup (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C))$
50	48 49	eqtri	$⊢ \{1_{𝑜}\} \times (B ⊔︀ C) = (\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \cup (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C))$
51	50	uneq2i	$⊢ (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (B ⊔︀ C)) = (\{\emptyset\} \times A) \cup ((\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \cup (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)))$
52		df-dju	$⊢ (A ⊔︀ (B ⊔︀ C)) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (B ⊔︀ C))$
53		unass	$⊢ ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (\{\emptyset\} \times B))) \cup (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)) = (\{\emptyset\} \times A) \cup ((\{1_{𝑜}\} \times (\{\emptyset\} \times B)) \cup (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C)))$
54	51 52 53	3eqtr4i	$⊢ (A ⊔︀ (B ⊔︀ C)) = ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times (\{\emptyset\} \times B))) \cup (\{1_{𝑜}\} \times (\{1_{𝑜}\} \times C))$
55	46 54	breqtrrdi	$⊢ (A \in V \land B \in W \land C \in X) \to ((A ⊔︀ B) ⊔︀ C) \approx (A ⊔︀ (B ⊔︀ C))$

Metamath Proof Explorer

Theorem djuassen

Proof