endisj

Description: Any two sets are equinumerous to two disjoint sets. Exercise 4.39 of Mendelson p. 255. (Contributed by NM, 16-Apr-2004)

	Ref	Expression
Hypotheses	endisj.1	$⊢ A \in V$
	endisj.2	$⊢ B \in V$
Assertion	endisj	$⊢ \exists x \exists y ((x \approx A \land y \approx B) \land x \cap y = \emptyset)$

Proof

Step	Hyp	Ref	Expression
1		endisj.1	$⊢ A \in V$
2		endisj.2	$⊢ B \in V$
3		0ex	$⊢ \emptyset \in V$
4	1 3	xpsnen	$⊢ (A \times \{\emptyset\}) \approx A$
5		1oex	$⊢ 1_{𝑜} \in V$
6	2 5	xpsnen	$⊢ (B \times \{1_{𝑜}\}) \approx B$
7	4 6	pm3.2i	$⊢ ((A \times \{\emptyset\}) \approx A \land (B \times \{1_{𝑜}\}) \approx B)$
8		xp01disj	$⊢ (A \times \{\emptyset\}) \cap (B \times \{1_{𝑜}\}) = \emptyset$
9		p0ex	$⊢ \{\emptyset\} \in V$
10	1 9	xpex	$⊢ A \times \{\emptyset\} \in V$
11		snex	$⊢ \{1_{𝑜}\} \in V$
12	2 11	xpex	$⊢ B \times \{1_{𝑜}\} \in V$
13		breq1	$⊢ x = A \times \{\emptyset\} \to (x \approx A \leftrightarrow (A \times \{\emptyset\}) \approx A)$
14		breq1	$⊢ y = B \times \{1_{𝑜}\} \to (y \approx B \leftrightarrow (B \times \{1_{𝑜}\}) \approx B)$
15	13 14	bi2anan9	$⊢ (x = A \times \{\emptyset\} \land y = B \times \{1_{𝑜}\}) \to ((x \approx A \land y \approx B) \leftrightarrow ((A \times \{\emptyset\}) \approx A \land (B \times \{1_{𝑜}\}) \approx B))$
16		ineq12	$⊢ (x = A \times \{\emptyset\} \land y = B \times \{1_{𝑜}\}) \to x \cap y = (A \times \{\emptyset\}) \cap (B \times \{1_{𝑜}\})$
17	16	eqeq1d	$⊢ (x = A \times \{\emptyset\} \land y = B \times \{1_{𝑜}\}) \to (x \cap y = \emptyset \leftrightarrow (A \times \{\emptyset\}) \cap (B \times \{1_{𝑜}\}) = \emptyset)$
18	15 17	anbi12d	$⊢ (x = A \times \{\emptyset\} \land y = B \times \{1_{𝑜}\}) \to (((x \approx A \land y \approx B) \land x \cap y = \emptyset) \leftrightarrow (((A \times \{\emptyset\}) \approx A \land (B \times \{1_{𝑜}\}) \approx B) \land (A \times \{\emptyset\}) \cap (B \times \{1_{𝑜}\}) = \emptyset))$
19	10 12 18	spc2ev	$⊢ (((A \times \{\emptyset\}) \approx A \land (B \times \{1_{𝑜}\}) \approx B) \land (A \times \{\emptyset\}) \cap (B \times \{1_{𝑜}\}) = \emptyset) \to \exists x \exists y ((x \approx A \land y \approx B) \land x \cap y = \emptyset)$
20	7 8 19	mp2an	$⊢ \exists x \exists y ((x \approx A \land y \approx B) \land x \cap y = \emptyset)$

Metamath Proof Explorer

Theorem endisj

Proof