Theorem disjif2

Description: Property of a disjoint collection: if B ( x ) and B ( Y ) = D have a common element Z , then x = Y . (Contributed by Thierry Arnoux, 6-Apr-2017)

	Ref	Expression
Hypotheses	disjif2.1	$$⊢\underset{\_}{Ⅎ}xA$$
	disjif2.2	$$⊢\underset{\_}{Ⅎ}xC$$
	disjif2.3	$$⊢x=Y\to B=C$$
Assertion	disjif2	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(x\in A\wedge Y\in A\right)\wedge \left(Z\in B\wedge Z\in C\right)\right)\to x=Y$$

Proof

Step	Hyp	Ref	Expression
1		disjif2.1	$$⊢\underset{\_}{Ⅎ}xA$$
2		disjif2.2	$$⊢\underset{\_}{Ⅎ}xC$$
3		disjif2.3	$$⊢x=Y\to B=C$$
4		inelcm	$$⊢\left(Z\in B\wedge Z\in C\right)\to B\cap C\ne \varnothing$$
5	1	disjorsf	$$⊢\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)$$
6		equequ1	$$⊢y=x\to \left(y=z\leftrightarrow x=z\right)$$
7		csbeq1	$$⊢y=x\to ⦋y/x⦌B=⦋x/x⦌B$$
8		csbid	$$⊢⦋x/x⦌B=B$$
9	7 8	eqtrdi	$$⊢y=x\to ⦋y/x⦌B=B$$
10	9	ineq1d	$$⊢y=x\to ⦋y/x⦌B\cap ⦋z/x⦌B=B\cap ⦋z/x⦌B$$
11	10	eqeq1d	$$⊢y=x\to \left(⦋y/x⦌B\cap ⦋z/x⦌B=\varnothing \leftrightarrow B\cap ⦋z/x⦌B=\varnothing \right)$$
12	6 11	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)$$
13		eqeq2	$$⊢z=Y\to \left(x=z\leftrightarrow x=Y\right)$$
14		nfcv	$$⊢\underset{\_}{Ⅎ}xY$$
15	14 2 3	csbhypf	$$⊢z=Y\to ⦋z/x⦌B=C$$
16	15	ineq2d	$$⊢z=Y\to B\cap ⦋z/x⦌B=B\cap C$$
17	16	eqeq1d	$$⊢z=Y\to \left(B\cap ⦋z/x⦌B=\varnothing \leftrightarrow B\cap C=\varnothing \right)$$
18	13 17	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)$$
19	12 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 B\cap C=\varnothing \right)\right)$$
20	5 19	biimtrid	$$⊢\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)$$
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 B\cap C=\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 B\cap C=\varnothing \right)$$
23	22	necon1ad	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(x\in A\wedge Y\in A\right)\right)\to \left(B\cap C\ne \varnothing \to x=Y\right)$$
24	23	3impia	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(x\in A\wedge Y\in A\right)\wedge B\cap C\ne \varnothing \right)\to x=Y$$
25	4 24	syl3an3	$$⊢\left(\underset{x\in A}{Disj}B\wedge \left(x\in A\wedge Y\in A\right)\wedge \left(Z\in B\wedge Z\in C\right)\right)\to x=Y$$