Theorem disji2f

Description: Property of a disjoint collection: if B ( x ) = C and B ( Y ) = D , and x =/= Y , then B and C are disjoint. (Contributed by Thierry Arnoux, 30-Dec-2016)

	Ref	Expression
Hypotheses	disjif.1	$$⊢\underset{\_}{Ⅎ}xC$$
	disjif.2	$$⊢x=Y\to B=C$$
Assertion	disji2f	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(x\in A\wedge Y\in A\right)\wedge x\ne Y\right)\to B\cap C=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		disjif.1	$$⊢\underset{\_}{Ⅎ}xC$$
2		disjif.2	$$⊢x=Y\to B=C$$
3		df-ne	$$⊢x\ne Y\leftrightarrow \neg x=Y$$
4		disjors	$$⊢\underset{x\in A}{Disj}B\leftrightarrow \forall y\in A\forall z\in A\left(y=z\vee ⦋y/x⦌B\cap ⦋z/x⦌B=\varnothing \right)$$
5		equequ1	$$⊢y=x\to \left(y=z\leftrightarrow x=z\right)$$
6		csbeq1	$$⊢y=x\to ⦋y/x⦌B=⦋x/x⦌B$$
7		csbid	$$⊢⦋x/x⦌B=B$$
8	6 7	eqtrdi	$$⊢y=x\to ⦋y/x⦌B=B$$
9	8	ineq1d	$$⊢y=x\to ⦋y/x⦌B\cap ⦋z/x⦌B=B\cap ⦋z/x⦌B$$
10	9	eqeq1d	$$⊢y=x\to \left(⦋y/x⦌B\cap ⦋z/x⦌B=\varnothing \leftrightarrow B\cap ⦋z/x⦌B=\varnothing \right)$$
11	5 10	orbi12d	$$⊢y=x\to \left(\left(y=z\vee ⦋y/x⦌B\cap ⦋z/x⦌B=\varnothing \right)\leftrightarrow \left(x=z\vee B\cap ⦋z/x⦌B=\varnothing \right)\right)$$
12		eqeq2	$$⊢z=Y\to \left(x=z\leftrightarrow x=Y\right)$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}xY$$
14	13 1 2	csbhypf	$$⊢z=Y\to ⦋z/x⦌B=C$$
15	14	ineq2d	$$⊢z=Y\to B\cap ⦋z/x⦌B=B\cap C$$
16	15	eqeq1d	$$⊢z=Y\to \left(B\cap ⦋z/x⦌B=\varnothing \leftrightarrow B\cap C=\varnothing \right)$$
17	12 16	orbi12d	$$⊢z=Y\to \left(\left(x=z\vee B\cap ⦋z/x⦌B=\varnothing \right)\leftrightarrow \left(x=Y\vee B\cap C=\varnothing \right)\right)$$
18	11 17	rspc2v	$$⊢\left(x\in A\wedge Y\in A\right)\to \left(\forall y\in A\forall z\in A\left(y=z\vee ⦋y/x⦌B\cap ⦋z/x⦌B=\varnothing \right)\to \left(x=Y\vee B\cap C=\varnothing \right)\right)$$
19	4 18	syl5bi	$$⊢\left(x\in A\wedge Y\in A\right)\to \left(\underset{x\in A}{Disj}B\to \left(x=Y\vee B\cap C=\varnothing \right)\right)$$
20	19	impcom	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(x\in A\wedge Y\in A\right)\right)\to \left(x=Y\vee B\cap C=\varnothing \right)$$
21	20	ord	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(x\in A\wedge Y\in A\right)\right)\to \left(\neg x=Y\to B\cap C=\varnothing \right)$$
22	3 21	syl5bi	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(x\in A\wedge Y\in A\right)\right)\to \left(x\ne Y\to B\cap C=\varnothing \right)$$
23	22	3impia	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(x\in A\wedge Y\in A\right)\wedge x\ne Y\right)\to B\cap C=\varnothing$$