Theorem 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 \mathrm{V}$$
	endisj.2	$$⊢B\in \mathrm{V}$$
Assertion	endisj	$$⊢\exists x\exists y\left(\left(x\approx A\wedge y\approx B\right)\wedge x\cap y=\varnothing \right)$$

Proof

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