Theorem disjenex

Description: Existence version of disjen . (Contributed by Mario Carneiro, 7-Feb-2015)

	Ref	Expression
Assertion	disjenex	$$⊢\left(A\in V\wedge B\in W\right)\to \exists x\left(A\cap x=\varnothing \wedge x\approx B\right)$$

Proof

Step	Hyp	Ref	Expression
1		simpr	$$⊢\left(A\in V\wedge B\in W\right)\to B\in W$$
2		snex	$$⊢\left\{𝒫\bigcup \mathrm{ran}A\right\}\in \mathrm{V}$$
3		xpexg	$$⊢\left(B\in W\wedge \left\{𝒫\bigcup \mathrm{ran}A\right\}\in \mathrm{V}\right)\to B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\in \mathrm{V}$$
4	1 2 3	sylancl	$$⊢\left(A\in V\wedge B\in W\right)\to B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\in \mathrm{V}$$
5		disjen	$$⊢\left(A\in V\wedge B\in W\right)\to \left(A\cap \left(B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\right)=\varnothing \wedge \left(B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\right)\approx B\right)$$
6		ineq2	$$⊢x=B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\to A\cap x=A\cap \left(B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\right)$$
7	6	eqeq1d	$$⊢x=B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\to \left(A\cap x=\varnothing \leftrightarrow A\cap \left(B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\right)=\varnothing \right)$$
8		breq1	$$⊢x=B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\to \left(x\approx B\leftrightarrow \left(B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\right)\approx B\right)$$
9	7 8	anbi12d	$$⊢x=B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\to \left(\left(A\cap x=\varnothing \wedge x\approx B\right)\leftrightarrow \left(A\cap \left(B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\right)=\varnothing \wedge \left(B\times \left\{𝒫\bigcup \mathrm{ran}A\right\}\right)\approx B\right)\right)$$
10	4 5 9	spcedv	$$⊢\left(A\in V\wedge B\in W\right)\to \exists x\left(A\cap x=\varnothing \wedge x\approx B\right)$$