djuen

Description: Disjoint unions of equinumerous sets are equinumerous. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

		Ref	Expression
	Assertion	djuen	$⊢ (A \approx B \land C \approx D) \to (A ⊔︀ C) \approx (B ⊔︀ D)$

Proof

Step	Hyp	Ref	Expression
1		0ex	$⊢ \emptyset \in V$
2		relen	$⊢ Rel \approx$
3	2	brrelex1i	$⊢ A \approx B \to A \in V$
4		xpsnen2g	$⊢ (\emptyset \in V \land A \in V) \to (\{\emptyset\} \times A) \approx A$
5	1 3 4	sylancr	$⊢ A \approx B \to (\{\emptyset\} \times A) \approx A$
6	2	brrelex2i	$⊢ A \approx B \to B \in V$
7		xpsnen2g	$⊢ (\emptyset \in V \land B \in V) \to (\{\emptyset\} \times B) \approx B$
8	1 6 7	sylancr	$⊢ A \approx B \to (\{\emptyset\} \times B) \approx B$
9	8	ensymd	$⊢ A \approx B \to B \approx (\{\emptyset\} \times B)$
10		entr	$⊢ (A \approx B \land B \approx (\{\emptyset\} \times B)) \to A \approx (\{\emptyset\} \times B)$
11	9 10	mpdan	$⊢ A \approx B \to A \approx (\{\emptyset\} \times B)$
12		entr	$⊢ ((\{\emptyset\} \times A) \approx A \land A \approx (\{\emptyset\} \times B)) \to (\{\emptyset\} \times A) \approx (\{\emptyset\} \times B)$
13	5 11 12	syl2anc	$⊢ A \approx B \to (\{\emptyset\} \times A) \approx (\{\emptyset\} \times B)$
14		1on	$⊢ 1_{𝑜} \in On$
15	2	brrelex1i	$⊢ C \approx D \to C \in V$
16		xpsnen2g	$⊢ (1_{𝑜} \in On \land C \in V) \to (\{1_{𝑜}\} \times C) \approx C$
17	14 15 16	sylancr	$⊢ C \approx D \to (\{1_{𝑜}\} \times C) \approx C$
18	2	brrelex2i	$⊢ C \approx D \to D \in V$
19		xpsnen2g	$⊢ (1_{𝑜} \in On \land D \in V) \to (\{1_{𝑜}\} \times D) \approx D$
20	14 18 19	sylancr	$⊢ C \approx D \to (\{1_{𝑜}\} \times D) \approx D$
21	20	ensymd	$⊢ C \approx D \to D \approx (\{1_{𝑜}\} \times D)$
22		entr	$⊢ (C \approx D \land D \approx (\{1_{𝑜}\} \times D)) \to C \approx (\{1_{𝑜}\} \times D)$
23	21 22	mpdan	$⊢ C \approx D \to C \approx (\{1_{𝑜}\} \times D)$
24		entr	$⊢ ((\{1_{𝑜}\} \times C) \approx C \land C \approx (\{1_{𝑜}\} \times D)) \to (\{1_{𝑜}\} \times C) \approx (\{1_{𝑜}\} \times D)$
25	17 23 24	syl2anc	$⊢ C \approx D \to (\{1_{𝑜}\} \times C) \approx (\{1_{𝑜}\} \times D)$
26		xp01disjl	$⊢ (\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times C) = \emptyset$
27		xp01disjl	$⊢ (\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times D) = \emptyset$
28		unen	$⊢ (((\{\emptyset\} \times A) \approx (\{\emptyset\} \times B) \land (\{1_{𝑜}\} \times C) \approx (\{1_{𝑜}\} \times D)) \land ((\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times C) = \emptyset \land (\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times D) = \emptyset)) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times C)) \approx ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times D))$
29	26 27 28	mpanr12	$⊢ ((\{\emptyset\} \times A) \approx (\{\emptyset\} \times B) \land (\{1_{𝑜}\} \times C) \approx (\{1_{𝑜}\} \times D)) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times C)) \approx ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times D))$
30	13 25 29	syl2an	$⊢ (A \approx B \land C \approx D) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times C)) \approx ((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times D))$
31		df-dju	$⊢ (A ⊔︀ C) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times C)$
32		df-dju	$⊢ (B ⊔︀ D) = (\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times D)$
33	30 31 32	3brtr4g	$⊢ (A \approx B \land C \approx D) \to (A ⊔︀ C) \approx (B ⊔︀ D)$

Metamath Proof Explorer

Theorem djuen

Proof