Theorem disjxpin

Description: Derive a disjunction over a Cartesian product from the disjunctions over its first and second elements. (Contributed by Thierry Arnoux, 9-Mar-2018)

	Ref	Expression
Hypotheses	disjxpin.1	$$⊢x=1^{st}\left(p\right)\to C=E$$
	disjxpin.2	$$⊢y=2^{nd}\left(p\right)\to D=F$$
	disjxpin.3	$$⊢\phi \to \underset{x\in A}{Disj}C$$
	disjxpin.4	$$⊢\phi \to \underset{y\in B}{Disj}D$$
Assertion	disjxpin	$$⊢\phi \to \underset{p\in A\times B}{Disj}\left(E\cap F\right)$$

Proof

Step	Hyp	Ref	Expression
1		disjxpin.1	$$⊢x=1^{st}\left(p\right)\to C=E$$
2		disjxpin.2	$$⊢y=2^{nd}\left(p\right)\to D=F$$
3		disjxpin.3	$$⊢\phi \to \underset{x\in A}{Disj}C$$
4		disjxpin.4	$$⊢\phi \to \underset{y\in B}{Disj}D$$
5		xp1st	$$⊢q\in \left(A\times B\right)\to 1^{st}\left(q\right)\in A$$
6	5	ad2antrl	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to 1^{st}\left(q\right)\in A$$
7		xp1st	$$⊢r\in \left(A\times B\right)\to 1^{st}\left(r\right)\in A$$
8	7	ad2antll	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to 1^{st}\left(r\right)\in A$$
9		simpl	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \phi$$
10		disjors	$$⊢\underset{x\in A}{Disj}C\leftrightarrow \forall a\in A\forall c\in A\left(a=c\vee ⦋a/x⦌C\cap ⦋c/x⦌C=\varnothing \right)$$
11	3 10	sylib	$$⊢\phi \to \forall a\in A\forall c\in A\left(a=c\vee ⦋a/x⦌C\cap ⦋c/x⦌C=\varnothing \right)$$
12		eqeq1	$$⊢a=1^{st}\left(q\right)\to \left(a=c\leftrightarrow 1^{st}\left(q\right)=c\right)$$
13		csbeq1	$$⊢a=1^{st}\left(q\right)\to ⦋a/x⦌C=⦋1^{st}\left(q\right)/x⦌C$$
14	13	ineq1d	$$⊢a=1^{st}\left(q\right)\to ⦋a/x⦌C\cap ⦋c/x⦌C=⦋1^{st}\left(q\right)/x⦌C\cap ⦋c/x⦌C$$
15	14	eqeq1d	$$⊢a=1^{st}\left(q\right)\to \left(⦋a/x⦌C\cap ⦋c/x⦌C=\varnothing \leftrightarrow ⦋1^{st}\left(q\right)/x⦌C\cap ⦋c/x⦌C=\varnothing \right)$$
16	12 15	orbi12d	$$⊢a=1^{st}\left(q\right)\to \left(\left(a=c\vee ⦋a/x⦌C\cap ⦋c/x⦌C=\varnothing \right)\leftrightarrow \left(1^{st}\left(q\right)=c\vee ⦋1^{st}\left(q\right)/x⦌C\cap ⦋c/x⦌C=\varnothing \right)\right)$$
17		eqeq2	$$⊢c=1^{st}\left(r\right)\to \left(1^{st}\left(q\right)=c\leftrightarrow 1^{st}\left(q\right)=1^{st}\left(r\right)\right)$$
18		csbeq1	$$⊢c=1^{st}\left(r\right)\to ⦋c/x⦌C=⦋1^{st}\left(r\right)/x⦌C$$
19	18	ineq2d	$$⊢c=1^{st}\left(r\right)\to ⦋1^{st}\left(q\right)/x⦌C\cap ⦋c/x⦌C=⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C$$
20	19	eqeq1d	$$⊢c=1^{st}\left(r\right)\to \left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋c/x⦌C=\varnothing \leftrightarrow ⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \right)$$
21	17 20	orbi12d	$$⊢c=1^{st}\left(r\right)\to \left(\left(1^{st}\left(q\right)=c\vee ⦋1^{st}\left(q\right)/x⦌C\cap ⦋c/x⦌C=\varnothing \right)\leftrightarrow \left(1^{st}\left(q\right)=1^{st}\left(r\right)\vee ⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \right)\right)$$
22	16 21	rspc2v	$$⊢\left(1^{st}\left(q\right)\in A\wedge 1^{st}\left(r\right)\in A\right)\to \left(\forall a\in A\forall c\in A\left(a=c\vee ⦋a/x⦌C\cap ⦋c/x⦌C=\varnothing \right)\to \left(1^{st}\left(q\right)=1^{st}\left(r\right)\vee ⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \right)\right)$$
23	11 22	syl5	$$⊢\left(1^{st}\left(q\right)\in A\wedge 1^{st}\left(r\right)\in A\right)\to \left(\phi \to \left(1^{st}\left(q\right)=1^{st}\left(r\right)\vee ⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \right)\right)$$
24	23	imp	$$⊢\left(\left(1^{st}\left(q\right)\in A\wedge 1^{st}\left(r\right)\in A\right)\wedge \phi \right)\to \left(1^{st}\left(q\right)=1^{st}\left(r\right)\vee ⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \right)$$
25	6 8 9 24	syl21anc	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(1^{st}\left(q\right)=1^{st}\left(r\right)\vee ⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \right)$$
26		xp2nd	$$⊢q\in \left(A\times B\right)\to 2^{nd}\left(q\right)\in B$$
27	26	ad2antrl	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to 2^{nd}\left(q\right)\in B$$
28		xp2nd	$$⊢r\in \left(A\times B\right)\to 2^{nd}\left(r\right)\in B$$
29	28	ad2antll	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to 2^{nd}\left(r\right)\in B$$
30		disjors	$$⊢\underset{y\in B}{Disj}D\leftrightarrow \forall b\in B\forall d\in B\left(b=d\vee ⦋b/y⦌D\cap ⦋d/y⦌D=\varnothing \right)$$
31	4 30	sylib	$$⊢\phi \to \forall b\in B\forall d\in B\left(b=d\vee ⦋b/y⦌D\cap ⦋d/y⦌D=\varnothing \right)$$
32		eqeq1	$$⊢b=2^{nd}\left(q\right)\to \left(b=d\leftrightarrow 2^{nd}\left(q\right)=d\right)$$
33		csbeq1	$$⊢b=2^{nd}\left(q\right)\to ⦋b/y⦌D=⦋2^{nd}\left(q\right)/y⦌D$$
34	33	ineq1d	$$⊢b=2^{nd}\left(q\right)\to ⦋b/y⦌D\cap ⦋d/y⦌D=⦋2^{nd}\left(q\right)/y⦌D\cap ⦋d/y⦌D$$
35	34	eqeq1d	$$⊢b=2^{nd}\left(q\right)\to \left(⦋b/y⦌D\cap ⦋d/y⦌D=\varnothing \leftrightarrow ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋d/y⦌D=\varnothing \right)$$
36	32 35	orbi12d	$$⊢b=2^{nd}\left(q\right)\to \left(\left(b=d\vee ⦋b/y⦌D\cap ⦋d/y⦌D=\varnothing \right)\leftrightarrow \left(2^{nd}\left(q\right)=d\vee ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋d/y⦌D=\varnothing \right)\right)$$
37		eqeq2	$$⊢d=2^{nd}\left(r\right)\to \left(2^{nd}\left(q\right)=d\leftrightarrow 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)$$
38		csbeq1	$$⊢d=2^{nd}\left(r\right)\to ⦋d/y⦌D=⦋2^{nd}\left(r\right)/y⦌D$$
39	38	ineq2d	$$⊢d=2^{nd}\left(r\right)\to ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋d/y⦌D=⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D$$
40	39	eqeq1d	$$⊢d=2^{nd}\left(r\right)\to \left(⦋2^{nd}\left(q\right)/y⦌D\cap ⦋d/y⦌D=\varnothing \leftrightarrow ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)$$
41	37 40	orbi12d	$$⊢d=2^{nd}\left(r\right)\to \left(\left(2^{nd}\left(q\right)=d\vee ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋d/y⦌D=\varnothing \right)\leftrightarrow \left(2^{nd}\left(q\right)=2^{nd}\left(r\right)\vee ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)$$
42	36 41	rspc2v	$$⊢\left(2^{nd}\left(q\right)\in B\wedge 2^{nd}\left(r\right)\in B\right)\to \left(\forall b\in B\forall d\in B\left(b=d\vee ⦋b/y⦌D\cap ⦋d/y⦌D=\varnothing \right)\to \left(2^{nd}\left(q\right)=2^{nd}\left(r\right)\vee ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)$$
43	31 42	syl5	$$⊢\left(2^{nd}\left(q\right)\in B\wedge 2^{nd}\left(r\right)\in B\right)\to \left(\phi \to \left(2^{nd}\left(q\right)=2^{nd}\left(r\right)\vee ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)$$
44	43	imp	$$⊢\left(\left(2^{nd}\left(q\right)\in B\wedge 2^{nd}\left(r\right)\in B\right)\wedge \phi \right)\to \left(2^{nd}\left(q\right)=2^{nd}\left(r\right)\vee ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)$$
45	27 29 9 44	syl21anc	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(2^{nd}\left(q\right)=2^{nd}\left(r\right)\vee ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)$$
46	25 45	jca	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\vee ⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \right)\wedge \left(2^{nd}\left(q\right)=2^{nd}\left(r\right)\vee ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)$$
47		anddi	$$⊢\left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\vee ⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \right)\wedge \left(2^{nd}\left(q\right)=2^{nd}\left(r\right)\vee ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\leftrightarrow \left(\left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\vee \left(\left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\right)$$
48	46 47	sylib	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(\left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\vee \left(\left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\right)$$
49		orass	$$⊢\left(\left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\vee \left(\left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\right)\leftrightarrow \left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\vee \left(\left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\right)\right)$$
50	48 49	sylib	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\vee \left(\left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\right)\right)$$
51		xpopth	$$⊢\left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\to \left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\leftrightarrow q=r\right)$$
52	51	adantl	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\leftrightarrow q=r\right)$$
53	52	biimpd	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\to q=r\right)$$
54		inss2	$$⊢\left(⦋q/p⦌E\cap ⦋r/p⦌E\right)\cap \left(⦋q/p⦌F\cap ⦋r/p⦌F\right)\subseteq ⦋q/p⦌F\cap ⦋r/p⦌F$$
55		csbin	$$⊢⦋q/p⦌\left(E\cap F\right)=⦋q/p⦌E\cap ⦋q/p⦌F$$
56		csbin	$$⊢⦋r/p⦌\left(E\cap F\right)=⦋r/p⦌E\cap ⦋r/p⦌F$$
57	55 56	ineq12i	$$⊢⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\left(⦋q/p⦌E\cap ⦋q/p⦌F\right)\cap \left(⦋r/p⦌E\cap ⦋r/p⦌F\right)$$
58		in4	$$⊢\left(⦋q/p⦌E\cap ⦋q/p⦌F\right)\cap \left(⦋r/p⦌E\cap ⦋r/p⦌F\right)=\left(⦋q/p⦌E\cap ⦋r/p⦌E\right)\cap \left(⦋q/p⦌F\cap ⦋r/p⦌F\right)$$
59	57 58	eqtri	$$⊢⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\left(⦋q/p⦌E\cap ⦋r/p⦌E\right)\cap \left(⦋q/p⦌F\cap ⦋r/p⦌F\right)$$
60		vex	$$⊢q\in \mathrm{V}$$
61		csbnestgw	$$⊢q\in \mathrm{V}\to ⦋q/p⦌⦋2^{nd}\left(p\right)/y⦌D=⦋⦋q/p⦌2^{nd}\left(p\right)/y⦌D$$
62	60 61	ax-mp	$$⊢⦋q/p⦌⦋2^{nd}\left(p\right)/y⦌D=⦋⦋q/p⦌2^{nd}\left(p\right)/y⦌D$$
63		fvex	$$⊢2^{nd}\left(p\right)\in \mathrm{V}$$
64	63 2	csbie	$$⊢⦋2^{nd}\left(p\right)/y⦌D=F$$
65	64	csbeq2i	$$⊢⦋q/p⦌⦋2^{nd}\left(p\right)/y⦌D=⦋q/p⦌F$$
66		csbfv	$$⊢⦋q/p⦌2^{nd}\left(p\right)=2^{nd}\left(q\right)$$
67		csbeq1	$$⊢⦋q/p⦌2^{nd}\left(p\right)=2^{nd}\left(q\right)\to ⦋⦋q/p⦌2^{nd}\left(p\right)/y⦌D=⦋2^{nd}\left(q\right)/y⦌D$$
68	66 67	ax-mp	$$⊢⦋⦋q/p⦌2^{nd}\left(p\right)/y⦌D=⦋2^{nd}\left(q\right)/y⦌D$$
69	62 65 68	3eqtr3ri	$$⊢⦋2^{nd}\left(q\right)/y⦌D=⦋q/p⦌F$$
70		vex	$$⊢r\in \mathrm{V}$$
71		csbnestgw	$$⊢r\in \mathrm{V}\to ⦋r/p⦌⦋2^{nd}\left(p\right)/y⦌D=⦋⦋r/p⦌2^{nd}\left(p\right)/y⦌D$$
72	70 71	ax-mp	$$⊢⦋r/p⦌⦋2^{nd}\left(p\right)/y⦌D=⦋⦋r/p⦌2^{nd}\left(p\right)/y⦌D$$
73	64	csbeq2i	$$⊢⦋r/p⦌⦋2^{nd}\left(p\right)/y⦌D=⦋r/p⦌F$$
74		csbfv	$$⊢⦋r/p⦌2^{nd}\left(p\right)=2^{nd}\left(r\right)$$
75		csbeq1	$$⊢⦋r/p⦌2^{nd}\left(p\right)=2^{nd}\left(r\right)\to ⦋⦋r/p⦌2^{nd}\left(p\right)/y⦌D=⦋2^{nd}\left(r\right)/y⦌D$$
76	74 75	ax-mp	$$⊢⦋⦋r/p⦌2^{nd}\left(p\right)/y⦌D=⦋2^{nd}\left(r\right)/y⦌D$$
77	72 73 76	3eqtr3ri	$$⊢⦋2^{nd}\left(r\right)/y⦌D=⦋r/p⦌F$$
78	69 77	ineq12i	$$⊢⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=⦋q/p⦌F\cap ⦋r/p⦌F$$
79	54 59 78	3sstr4i	$$⊢⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)\subseteq ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D$$
80		sseq0	$$⊢\left(⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)\subseteq ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D\wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\to ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing$$
81	79 80	mpan	$$⊢⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \to ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing$$
82	81	a1i	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \to ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing \right)$$
83	82	adantld	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\to ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing \right)$$
84		inss1	$$⊢\left(⦋q/p⦌E\cap ⦋r/p⦌E\right)\cap \left(⦋q/p⦌F\cap ⦋r/p⦌F\right)\subseteq ⦋q/p⦌E\cap ⦋r/p⦌E$$
85		csbnestgw	$$⊢q\in \mathrm{V}\to ⦋q/p⦌⦋1^{st}\left(p\right)/x⦌C=⦋⦋q/p⦌1^{st}\left(p\right)/x⦌C$$
86	60 85	ax-mp	$$⊢⦋q/p⦌⦋1^{st}\left(p\right)/x⦌C=⦋⦋q/p⦌1^{st}\left(p\right)/x⦌C$$
87		fvex	$$⊢1^{st}\left(p\right)\in \mathrm{V}$$
88	87 1	csbie	$$⊢⦋1^{st}\left(p\right)/x⦌C=E$$
89	88	csbeq2i	$$⊢⦋q/p⦌⦋1^{st}\left(p\right)/x⦌C=⦋q/p⦌E$$
90		csbfv	$$⊢⦋q/p⦌1^{st}\left(p\right)=1^{st}\left(q\right)$$
91		csbeq1	$$⊢⦋q/p⦌1^{st}\left(p\right)=1^{st}\left(q\right)\to ⦋⦋q/p⦌1^{st}\left(p\right)/x⦌C=⦋1^{st}\left(q\right)/x⦌C$$
92	90 91	ax-mp	$$⊢⦋⦋q/p⦌1^{st}\left(p\right)/x⦌C=⦋1^{st}\left(q\right)/x⦌C$$
93	86 89 92	3eqtr3ri	$$⊢⦋1^{st}\left(q\right)/x⦌C=⦋q/p⦌E$$
94		csbnestgw	$$⊢r\in \mathrm{V}\to ⦋r/p⦌⦋1^{st}\left(p\right)/x⦌C=⦋⦋r/p⦌1^{st}\left(p\right)/x⦌C$$
95	70 94	ax-mp	$$⊢⦋r/p⦌⦋1^{st}\left(p\right)/x⦌C=⦋⦋r/p⦌1^{st}\left(p\right)/x⦌C$$
96	88	csbeq2i	$$⊢⦋r/p⦌⦋1^{st}\left(p\right)/x⦌C=⦋r/p⦌E$$
97		csbfv	$$⊢⦋r/p⦌1^{st}\left(p\right)=1^{st}\left(r\right)$$
98		csbeq1	$$⊢⦋r/p⦌1^{st}\left(p\right)=1^{st}\left(r\right)\to ⦋⦋r/p⦌1^{st}\left(p\right)/x⦌C=⦋1^{st}\left(r\right)/x⦌C$$
99	97 98	ax-mp	$$⊢⦋⦋r/p⦌1^{st}\left(p\right)/x⦌C=⦋1^{st}\left(r\right)/x⦌C$$
100	95 96 99	3eqtr3ri	$$⊢⦋1^{st}\left(r\right)/x⦌C=⦋r/p⦌E$$
101	93 100	ineq12i	$$⊢⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=⦋q/p⦌E\cap ⦋r/p⦌E$$
102	84 59 101	3sstr4i	$$⊢⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)\subseteq ⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C$$
103		sseq0	$$⊢\left(⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)\subseteq ⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C\wedge ⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \right)\to ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing$$
104	102 103	mpan	$$⊢⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \to ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing$$
105	104	a1i	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \to ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing \right)$$
106	105	adantrd	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(\left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\to ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing \right)$$
107	82	adantld	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(\left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\to ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing \right)$$
108	106 107	jaod	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(\left(\left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\to ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing \right)$$
109	83 108	jaod	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(\left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\vee \left(\left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\right)\to ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing \right)$$
110	53 109	orim12d	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(\left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(\left(1^{st}\left(q\right)=1^{st}\left(r\right)\wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\vee \left(\left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge 2^{nd}\left(q\right)=2^{nd}\left(r\right)\right)\vee \left(⦋1^{st}\left(q\right)/x⦌C\cap ⦋1^{st}\left(r\right)/x⦌C=\varnothing \wedge ⦋2^{nd}\left(q\right)/y⦌D\cap ⦋2^{nd}\left(r\right)/y⦌D=\varnothing \right)\right)\right)\right)\to \left(q=r\vee ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing \right)\right)$$
111	50 110	mpd	$$⊢\left(\phi \wedge \left(q\in \left(A\times B\right)\wedge r\in \left(A\times B\right)\right)\right)\to \left(q=r\vee ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing \right)$$
112	111	ralrimivva	$$⊢\phi \to \forall q\in \left(A\times B\right)\forall r\in \left(A\times B\right)\left(q=r\vee ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing \right)$$
113		disjors	$$⊢\underset{p\in A\times B}{Disj}\left(E\cap F\right)\leftrightarrow \forall q\in \left(A\times B\right)\forall r\in \left(A\times B\right)\left(q=r\vee ⦋q/p⦌\left(E\cap F\right)\cap ⦋r/p⦌\left(E\cap F\right)=\varnothing \right)$$
114	112 113	sylibr	$$⊢\phi \to \underset{p\in A\times B}{Disj}\left(E\cap F\right)$$