endjudisj

Description: Equinumerosity of a disjoint union and a union of two disjoint sets. (Contributed by NM, 5-Apr-2007)

		Ref	Expression
	Assertion	endjudisj	$⊢ (A \in V \land B \in W \land A \cap B = \emptyset) \to (A ⊔︀ B) \approx (A \cup B)$

Step	Hyp	Ref	Expression
1		df-dju	$⊢ (A ⊔︀ B) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)$
2		0ex	$⊢ \emptyset \in V$
3		xpsnen2g	$⊢ (\emptyset \in V \land A \in V) \to (\{\emptyset\} \times A) \approx A$
4	2 3	mpan	$⊢ A \in V \to (\{\emptyset\} \times A) \approx A$
5		1on	$⊢ 1_{𝑜} \in On$
6		xpsnen2g	$⊢ (1_{𝑜} \in On \land B \in W) \to (\{1_{𝑜}\} \times B) \approx B$
7	5 6	mpan	$⊢ B \in W \to (\{1_{𝑜}\} \times B) \approx B$
8	4 7	anim12i	$⊢ (A \in V \land B \in W) \to ((\{\emptyset\} \times A) \approx A \land (\{1_{𝑜}\} \times B) \approx B)$
9		xp01disjl	$⊢ (\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times B) = \emptyset$
10	9	jctl	$⊢ A \cap B = \emptyset \to ((\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times B) = \emptyset \land A \cap B = \emptyset)$
11		unen	$⊢ (((\{\emptyset\} \times A) \approx A \land (\{1_{𝑜}\} \times B) \approx B) \land ((\{\emptyset\} \times A) \cap (\{1_{𝑜}\} \times B) = \emptyset \land A \cap B = \emptyset)) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \approx (A \cup B)$
12	8 10 11	syl2an	$⊢ ((A \in V \land B \in W) \land A \cap B = \emptyset) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \approx (A \cup B)$
13	12	3impa	$⊢ (A \in V \land B \in W \land A \cap B = \emptyset) \to ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)) \approx (A \cup B)$
14	1 13	eqbrtrid	$⊢ (A \in V \land B \in W \land A \cap B = \emptyset) \to (A ⊔︀ B) \approx (A \cup B)$

Metamath Proof Explorer