Theorem disji2

Description: Property of a disjoint collection: if B ( X ) = C and B ( Y ) = D , and X =/= Y , then C and D are disjoint. (Contributed by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Hypotheses	disji.1	$$⊢x=X\to B=C$$
	disji.2	$$⊢x=Y\to B=D$$
Assertion	disji2	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(X\in A\wedge Y\in A\right)\wedge X\ne Y\right)\to C\cap D=\varnothing$$

Proof

Step	Hyp	Ref	Expression
1		disji.1	$$⊢x=X\to B=C$$
2		disji.2	$$⊢x=Y\to B=D$$
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		eqeq1	$$⊢y=X\to \left(y=z\leftrightarrow X=z\right)$$
6		nfcv	$$⊢\underset{\_}{Ⅎ}xX$$
7		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
8	6 7 1	csbhypf	$$⊢y=X\to ⦋y/x⦌B=C$$
9	8	ineq1d	$$⊢y=X\to ⦋y/x⦌B\cap ⦋z/x⦌B=C\cap ⦋z/x⦌B$$
10	9	eqeq1d	$$⊢y=X\to \left(⦋y/x⦌B\cap ⦋z/x⦌B=\varnothing \leftrightarrow C\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 C\cap ⦋z/x⦌B=\varnothing \right)\right)$$
12		eqeq2	$$⊢z=Y\to \left(X=z\leftrightarrow X=Y\right)$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}xY$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}xD$$
15	13 14 2	csbhypf	$$⊢z=Y\to ⦋z/x⦌B=D$$
16	15	ineq2d	$$⊢z=Y\to C\cap ⦋z/x⦌B=C\cap D$$
17	16	eqeq1d	$$⊢z=Y\to \left(C\cap ⦋z/x⦌B=\varnothing \leftrightarrow C\cap D=\varnothing \right)$$
18	12 17	orbi12d	$$⊢z=Y\to \left(\left(X=z\vee C\cap ⦋z/x⦌B=\varnothing \right)\leftrightarrow \left(X=Y\vee C\cap D=\varnothing \right)\right)$$
19	11 18	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 C\cap D=\varnothing \right)\right)$$
20	4 19	syl5bi	$$⊢\left(X\in A\wedge Y\in A\right)\to \left(\underset{x\in A}{Disj}B\to \left(X=Y\vee C\cap D=\varnothing \right)\right)$$
21	20	impcom	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(X\in A\wedge Y\in A\right)\right)\to \left(X=Y\vee C\cap D=\varnothing \right)$$
22	21	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 C\cap D=\varnothing \right)$$
23	3 22	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 C\cap D=\varnothing \right)$$
24	23	3impia	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(X\in A\wedge Y\in A\right)\wedge X\ne Y\right)\to C\cap D=\varnothing$$