Theorem disjprg

Description: A pair collection is disjoint iff the two sets in the family have empty intersection. (Contributed by Mario Carneiro, 14-Nov-2016)

	Ref	Expression
Hypotheses	disjprg.1	$$⊢x=A\to C=D$$
	disjprg.2	$$⊢x=B\to C=E$$
Assertion	disjprg	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(\underset{x\in \left\{A,B\right\}}{Disj}C\leftrightarrow D\cap E=\varnothing \right)$$

Proof

Step	Hyp	Ref	Expression
1		disjprg.1	$$⊢x=A\to C=D$$
2		disjprg.2	$$⊢x=B\to C=E$$
3		eqeq1	$$⊢y=A\to \left(y=z\leftrightarrow A=z\right)$$
4		nfcv	$$⊢\underset{\_}{Ⅎ}xA$$
5		nfcv	$$⊢\underset{\_}{Ⅎ}xD$$
6	4 5 1	csbhypf	$$⊢y=A\to ⦋y/x⦌C=D$$
7	6	ineq1d	$$⊢y=A\to ⦋y/x⦌C\cap ⦋z/x⦌C=D\cap ⦋z/x⦌C$$
8	7	eqeq1d	$$⊢y=A\to \left(⦋y/x⦌C\cap ⦋z/x⦌C=\varnothing \leftrightarrow D\cap ⦋z/x⦌C=\varnothing \right)$$
9	3 8	orbi12d	$$⊢y=A\to \left(\left(y=z\vee ⦋y/x⦌C\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \left(A=z\vee D\cap ⦋z/x⦌C=\varnothing \right)\right)$$
10	9	ralbidv	$$⊢y=A\to \left(\forall z\in \left\{A,B\right\}\left(y=z\vee ⦋y/x⦌C\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \forall z\in \left\{A,B\right\}\left(A=z\vee D\cap ⦋z/x⦌C=\varnothing \right)\right)$$
11		eqeq1	$$⊢y=B\to \left(y=z\leftrightarrow B=z\right)$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}xB$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}xE$$
14	12 13 2	csbhypf	$$⊢y=B\to ⦋y/x⦌C=E$$
15	14	ineq1d	$$⊢y=B\to ⦋y/x⦌C\cap ⦋z/x⦌C=E\cap ⦋z/x⦌C$$
16	15	eqeq1d	$$⊢y=B\to \left(⦋y/x⦌C\cap ⦋z/x⦌C=\varnothing \leftrightarrow E\cap ⦋z/x⦌C=\varnothing \right)$$
17	11 16	orbi12d	$$⊢y=B\to \left(\left(y=z\vee ⦋y/x⦌C\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \left(B=z\vee E\cap ⦋z/x⦌C=\varnothing \right)\right)$$
18	17	ralbidv	$$⊢y=B\to \left(\forall z\in \left\{A,B\right\}\left(y=z\vee ⦋y/x⦌C\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \forall z\in \left\{A,B\right\}\left(B=z\vee E\cap ⦋z/x⦌C=\varnothing \right)\right)$$
19	10 18	ralprg	$$⊢\left(A\in V\wedge B\in V\right)\to \left(\forall y\in \left\{A,B\right\}\forall z\in \left\{A,B\right\}\left(y=z\vee ⦋y/x⦌C\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \left(\forall z\in \left\{A,B\right\}\left(A=z\vee D\cap ⦋z/x⦌C=\varnothing \right)\wedge \forall z\in \left\{A,B\right\}\left(B=z\vee E\cap ⦋z/x⦌C=\varnothing \right)\right)\right)$$
20	19	3adant3	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(\forall y\in \left\{A,B\right\}\forall z\in \left\{A,B\right\}\left(y=z\vee ⦋y/x⦌C\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \left(\forall z\in \left\{A,B\right\}\left(A=z\vee D\cap ⦋z/x⦌C=\varnothing \right)\wedge \forall z\in \left\{A,B\right\}\left(B=z\vee E\cap ⦋z/x⦌C=\varnothing \right)\right)\right)$$
21		id	$$⊢z=A\to z=A$$
22	21	eqcomd	$$⊢z=A\to A=z$$
23	22	orcd	$$⊢z=A\to \left(A=z\vee D\cap ⦋z/x⦌C=\varnothing \right)$$
24		trud	$$⊢z=A\to \top$$
25	23 24	2thd	$$⊢z=A\to \left(\left(A=z\vee D\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \top \right)$$
26		eqeq2	$$⊢z=B\to \left(A=z\leftrightarrow A=B\right)$$
27	12 13 2	csbhypf	$$⊢z=B\to ⦋z/x⦌C=E$$
28	27	ineq2d	$$⊢z=B\to D\cap ⦋z/x⦌C=D\cap E$$
29	28	eqeq1d	$$⊢z=B\to \left(D\cap ⦋z/x⦌C=\varnothing \leftrightarrow D\cap E=\varnothing \right)$$
30	26 29	orbi12d	$$⊢z=B\to \left(\left(A=z\vee D\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \left(A=B\vee D\cap E=\varnothing \right)\right)$$
31	25 30	ralprg	$$⊢\left(A\in V\wedge B\in V\right)\to \left(\forall z\in \left\{A,B\right\}\left(A=z\vee D\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \left(\top \wedge \left(A=B\vee D\cap E=\varnothing \right)\right)\right)$$
32	31	3adant3	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(\forall z\in \left\{A,B\right\}\left(A=z\vee D\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \left(\top \wedge \left(A=B\vee D\cap E=\varnothing \right)\right)\right)$$
33		simp3	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to A\ne B$$
34	33	neneqd	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \neg A=B$$
35		biorf	$$⊢\neg A=B\to \left(D\cap E=\varnothing \leftrightarrow \left(A=B\vee D\cap E=\varnothing \right)\right)$$
36	34 35	syl	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(D\cap E=\varnothing \leftrightarrow \left(A=B\vee D\cap E=\varnothing \right)\right)$$
37		tru	$$⊢\top$$
38	37	biantrur	$$⊢\left(A=B\vee D\cap E=\varnothing \right)\leftrightarrow \left(\top \wedge \left(A=B\vee D\cap E=\varnothing \right)\right)$$
39	36 38	syl6bb	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(D\cap E=\varnothing \leftrightarrow \left(\top \wedge \left(A=B\vee D\cap E=\varnothing \right)\right)\right)$$
40	32 39	bitr4d	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(\forall z\in \left\{A,B\right\}\left(A=z\vee D\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow D\cap E=\varnothing \right)$$
41		eqeq2	$$⊢z=A\to \left(B=z\leftrightarrow B=A\right)$$
42		eqcom	$$⊢B=A\leftrightarrow A=B$$
43	41 42	syl6bb	$$⊢z=A\to \left(B=z\leftrightarrow A=B\right)$$
44	4 5 1	csbhypf	$$⊢z=A\to ⦋z/x⦌C=D$$
45	44	ineq2d	$$⊢z=A\to E\cap ⦋z/x⦌C=E\cap D$$
46		incom	$$⊢E\cap D=D\cap E$$
47	45 46	syl6eq	$$⊢z=A\to E\cap ⦋z/x⦌C=D\cap E$$
48	47	eqeq1d	$$⊢z=A\to \left(E\cap ⦋z/x⦌C=\varnothing \leftrightarrow D\cap E=\varnothing \right)$$
49	43 48	orbi12d	$$⊢z=A\to \left(\left(B=z\vee E\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \left(A=B\vee D\cap E=\varnothing \right)\right)$$
50		id	$$⊢z=B\to z=B$$
51	50	eqcomd	$$⊢z=B\to B=z$$
52	51	orcd	$$⊢z=B\to \left(B=z\vee E\cap ⦋z/x⦌C=\varnothing \right)$$
53		trud	$$⊢z=B\to \top$$
54	52 53	2thd	$$⊢z=B\to \left(\left(B=z\vee E\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \top \right)$$
55	49 54	ralprg	$$⊢\left(A\in V\wedge B\in V\right)\to \left(\forall z\in \left\{A,B\right\}\left(B=z\vee E\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \left(\left(A=B\vee D\cap E=\varnothing \right)\wedge \top \right)\right)$$
56	55	3adant3	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(\forall z\in \left\{A,B\right\}\left(B=z\vee E\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \left(\left(A=B\vee D\cap E=\varnothing \right)\wedge \top \right)\right)$$
57	37	biantru	$$⊢\left(A=B\vee D\cap E=\varnothing \right)\leftrightarrow \left(\left(A=B\vee D\cap E=\varnothing \right)\wedge \top \right)$$
58	36 57	syl6bb	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(D\cap E=\varnothing \leftrightarrow \left(\left(A=B\vee D\cap E=\varnothing \right)\wedge \top \right)\right)$$
59	56 58	bitr4d	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(\forall z\in \left\{A,B\right\}\left(B=z\vee E\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow D\cap E=\varnothing \right)$$
60	40 59	anbi12d	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(\left(\forall z\in \left\{A,B\right\}\left(A=z\vee D\cap ⦋z/x⦌C=\varnothing \right)\wedge \forall z\in \left\{A,B\right\}\left(B=z\vee E\cap ⦋z/x⦌C=\varnothing \right)\right)\leftrightarrow \left(D\cap E=\varnothing \wedge D\cap E=\varnothing \right)\right)$$
61	20 60	bitrd	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(\forall y\in \left\{A,B\right\}\forall z\in \left\{A,B\right\}\left(y=z\vee ⦋y/x⦌C\cap ⦋z/x⦌C=\varnothing \right)\leftrightarrow \left(D\cap E=\varnothing \wedge D\cap E=\varnothing \right)\right)$$
62		disjors	$$⊢\underset{x\in \left\{A,B\right\}}{Disj}C\leftrightarrow \forall y\in \left\{A,B\right\}\forall z\in \left\{A,B\right\}\left(y=z\vee ⦋y/x⦌C\cap ⦋z/x⦌C=\varnothing \right)$$
63		pm4.24	$$⊢D\cap E=\varnothing \leftrightarrow \left(D\cap E=\varnothing \wedge D\cap E=\varnothing \right)$$
64	61 62 63	3bitr4g	$$⊢\left(A\in V\wedge B\in V\wedge A\ne B\right)\to \left(\underset{x\in \left\{A,B\right\}}{Disj}C\leftrightarrow D\cap E=\varnothing \right)$$