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} (p) \to C = E$
	disjxpin.2	$⊢ y = 2^{nd} (p) \to D = F$
	disjxpin.3	$⊢ φ \to \underset{x \in A}{Disj} C$
	disjxpin.4	$⊢ φ \to \underset{y \in B}{Disj} D$
Assertion	disjxpin	$⊢ φ \to \underset{p \in A \times B}{Disj} (E \cap F)$

Proof

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

Metamath Proof Explorer

Theorem disjxpin

Proof