Theorem disjnf

Description: In case x is not free in B , disjointness is not so interesting since it reduces to cases where A is a singleton. (Google Groups discussion with Peter Mazsa.) (Contributed by Thierry Arnoux, 26-Jul-2018)

	Ref	Expression
Assertion	disjnf	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \left(B=\varnothing \vee {\exists }^{*}xx\in A\right)$$

Proof

Step	Hyp	Ref	Expression
1		inidm	$$⊢B\cap B=B$$
2	1	eqeq1i	$$⊢B\cap B=\varnothing \leftrightarrow B=\varnothing$$
3	2	orbi1i	$$⊢\left(B\cap B=\varnothing \vee \forall x\in A\forall y\in Ax=y\right)\leftrightarrow \left(B=\varnothing \vee \forall x\in A\forall y\in Ax=y\right)$$
4		eqidd	$$⊢x=y\to B=B$$
5	4	disjor	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall x\in A\forall y\in A\left(x=y\vee B\cap B=\varnothing \right)$$
6		orcom	$$⊢\left(x=y\vee B\cap B=\varnothing \right)\leftrightarrow \left(B\cap B=\varnothing \vee x=y\right)$$
7	6	ralbii	$$⊢\forall y\in A\left(x=y\vee B\cap B=\varnothing \right)\leftrightarrow \forall y\in A\left(B\cap B=\varnothing \vee x=y\right)$$
8		r19.32v	$$⊢\forall y\in A\left(B\cap B=\varnothing \vee x=y\right)\leftrightarrow \left(B\cap B=\varnothing \vee \forall y\in Ax=y\right)$$
9	7 8	bitri	$$⊢\forall y\in A\left(x=y\vee B\cap B=\varnothing \right)\leftrightarrow \left(B\cap B=\varnothing \vee \forall y\in Ax=y\right)$$
10	9	ralbii	$$⊢\forall x\in A\forall y\in A\left(x=y\vee B\cap B=\varnothing \right)\leftrightarrow \forall x\in A\left(B\cap B=\varnothing \vee \forall y\in Ax=y\right)$$
11		r19.32v	$$⊢\forall x\in A\left(B\cap B=\varnothing \vee \forall y\in Ax=y\right)\leftrightarrow \left(B\cap B=\varnothing \vee \forall x\in A\forall y\in Ax=y\right)$$
12	5 10 11	3bitri	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \left(B\cap B=\varnothing \vee \forall x\in A\forall y\in Ax=y\right)$$
13		moel	$$⊢{\exists }^{*}xx\in A\leftrightarrow \forall x\in A\forall y\in Ax=y$$
14	13	orbi2i	$$⊢\left(B=\varnothing \vee {\exists }^{*}xx\in A\right)\leftrightarrow \left(B=\varnothing \vee \forall x\in A\forall y\in Ax=y\right)$$
15	3 12 14	3bitr4i	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \left(B=\varnothing \vee {\exists }^{*}xx\in A\right)$$