Theorem ndisj2

Description: A non-disjointness condition. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypothesis	ndisj2.1	$$⊢x=y\to B=C$$
Assertion	ndisj2	$$⊢\neg \underset{x\in A}{Disj}B\leftrightarrow \exists x\in A\exists y\in A\left(x\ne y\wedge B\cap C\ne \varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		ndisj2.1	$$⊢x=y\to B=C$$
2	1	disjor	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall x\in A\forall y\in A\left(x=y\vee B\cap C=\varnothing \right)$$
3	2	notbii	$$⊢\neg \underset{x\in A}{Disj}B\leftrightarrow \neg \forall x\in A\forall y\in A\left(x=y\vee B\cap C=\varnothing \right)$$
4		rexnal	$$⊢\exists x\in A\neg \forall y\in A\left(x=y\vee B\cap C=\varnothing \right)\leftrightarrow \neg \forall x\in A\forall y\in A\left(x=y\vee B\cap C=\varnothing \right)$$
5		rexnal	$$⊢\exists y\in A\neg \left(x=y\vee B\cap C=\varnothing \right)\leftrightarrow \neg \forall y\in A\left(x=y\vee B\cap C=\varnothing \right)$$
6		ioran	$$⊢\neg \left(x=y\vee B\cap C=\varnothing \right)\leftrightarrow \left(\neg x=y\wedge \neg B\cap C=\varnothing \right)$$
7		df-ne	$$⊢x\ne y\leftrightarrow \neg x=y$$
8		df-ne	$$⊢B\cap C\ne \varnothing \leftrightarrow \neg B\cap C=\varnothing$$
9	7 8	anbi12i	$$⊢\left(x\ne y\wedge B\cap C\ne \varnothing \right)\leftrightarrow \left(\neg x=y\wedge \neg B\cap C=\varnothing \right)$$
10	6 9	bitr4i	$$⊢\neg \left(x=y\vee B\cap C=\varnothing \right)\leftrightarrow \left(x\ne y\wedge B\cap C\ne \varnothing \right)$$
11	10	rexbii	$$⊢\exists y\in A\neg \left(x=y\vee B\cap C=\varnothing \right)\leftrightarrow \exists y\in A\left(x\ne y\wedge B\cap C\ne \varnothing \right)$$
12	5 11	bitr3i	$$⊢\neg \forall y\in A\left(x=y\vee B\cap C=\varnothing \right)\leftrightarrow \exists y\in A\left(x\ne y\wedge B\cap C\ne \varnothing \right)$$
13	12	rexbii	$$⊢\exists x\in A\neg \forall y\in A\left(x=y\vee B\cap C=\varnothing \right)\leftrightarrow \exists x\in A\exists y\in A\left(x\ne y\wedge B\cap C\ne \varnothing \right)$$
14	3 4 13	3bitr2i	$$⊢\neg \underset{x\in A}{Disj}B\leftrightarrow \exists x\in A\exists y\in A\left(x\ne y\wedge B\cap C\ne \varnothing \right)$$