disjxpin - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > disjxpin		Structured version Visualization version GIF version

Theorem disjxpin 30340

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

**Hypotheses**
Ref	Expression
disjxpin.1	⊢ (𝑥 = (1^st ‘𝑝) → 𝐶 = 𝐸)
disjxpin.2	⊢ (𝑦 = (2^nd ‘𝑝) → 𝐷 = 𝐹)
disjxpin.3	⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐶)
disjxpin.4	⊢ (𝜑 → Disj 𝑦 ∈ 𝐵 𝐷)

**Assertion**
Ref	Expression
disjxpin	⊢ (𝜑 → Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹))

Distinct variable groups: 𝑥,𝑝,𝐴 𝑦,𝑝,𝐵 𝐶,𝑝 𝐷,𝑝 𝑥,𝐸 𝑦,𝐹 Allowed substitution hints: 𝜑(𝑥,𝑦,𝑝) 𝐴(𝑦) 𝐵(𝑥) 𝐶(𝑥,𝑦) 𝐷(𝑥,𝑦) 𝐸(𝑦,𝑝) 𝐹(𝑥,𝑝)

Proof of Theorem disjxpin Dummy variables 𝑎 𝑐 𝑞 𝑟 𝑏 𝑑 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xp1st 7723	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝐴 × 𝐵) → (1^st ‘𝑞) ∈ 𝐴)
2	1	ad2antrl 726	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (1^st ‘𝑞) ∈ 𝐴)
3		xp1st 7723	. . . . . . . . 9 ⊢ (𝑟 ∈ (𝐴 × 𝐵) → (1^st ‘𝑟) ∈ 𝐴)
4	3	ad2antll 727	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (1^st ‘𝑟) ∈ 𝐴)
5		simpl 485	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → 𝜑)
6		disjxpin.3	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐶)
7		disjors 5049	. . . . . . . . . . 11 ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
8	6, 7	sylib 220	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
9		eqeq1 2827	. . . . . . . . . . . 12 ⊢ (𝑎 = (1^st ‘𝑞) → (𝑎 = 𝑐 ↔ (1^st ‘𝑞) = 𝑐))
10		csbeq1 3888	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (1^st ‘𝑞) → ⦋𝑎 / 𝑥⦌𝐶 = ⦋(1^st ‘𝑞) / 𝑥⦌𝐶)
11	10	ineq1d 4190	. . . . . . . . . . . . 13 ⊢ (𝑎 = (1^st ‘𝑞) → (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶))
12	11	eqeq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑎 = (1^st ‘𝑞) → ((⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅ ↔ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
13	9, 12	orbi12d 915	. . . . . . . . . . 11 ⊢ (𝑎 = (1^st ‘𝑞) → ((𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) ↔ ((1^st ‘𝑞) = 𝑐 ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅)))
14		eqeq2 2835	. . . . . . . . . . . 12 ⊢ (𝑐 = (1^st ‘𝑟) → ((1^st ‘𝑞) = 𝑐 ↔ (1^st ‘𝑞) = (1^st ‘𝑟)))
15		csbeq1 3888	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (1^st ‘𝑟) → ⦋𝑐 / 𝑥⦌𝐶 = ⦋(1^st ‘𝑟) / 𝑥⦌𝐶)
16	15	ineq2d 4191	. . . . . . . . . . . . 13 ⊢ (𝑐 = (1^st ‘𝑟) → (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶))
17	16	eqeq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑐 = (1^st ‘𝑟) → ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅ ↔ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
18	14, 17	orbi12d 915	. . . . . . . . . . 11 ⊢ (𝑐 = (1^st ‘𝑟) → (((1^st ‘𝑞) = 𝑐 ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) ↔ ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅)))
19	13, 18	rspc2v 3635	. . . . . . . . . 10 ⊢ (((1^st ‘𝑞) ∈ 𝐴 ∧ (1^st ‘𝑟) ∈ 𝐴) → (∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅)))
20	8, 19	syl5 34	. . . . . . . . 9 ⊢ (((1^st ‘𝑞) ∈ 𝐴 ∧ (1^st ‘𝑟) ∈ 𝐴) → (𝜑 → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅)))
21	20	imp 409	. . . . . . . 8 ⊢ ((((1^st ‘𝑞) ∈ 𝐴 ∧ (1^st ‘𝑟) ∈ 𝐴) ∧ 𝜑) → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
22	2, 4, 5, 21	syl21anc 835	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
23		xp2nd 7724	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝐴 × 𝐵) → (2^nd ‘𝑞) ∈ 𝐵)
24	23	ad2antrl 726	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (2^nd ‘𝑞) ∈ 𝐵)
25		xp2nd 7724	. . . . . . . . 9 ⊢ (𝑟 ∈ (𝐴 × 𝐵) → (2^nd ‘𝑟) ∈ 𝐵)
26	25	ad2antll 727	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (2^nd ‘𝑟) ∈ 𝐵)
27		disjxpin.4	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑦 ∈ 𝐵 𝐷)
28		disjors 5049	. . . . . . . . . . 11 ⊢ (Disj 𝑦 ∈ 𝐵 𝐷 ↔ ∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
29	27, 28	sylib 220	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
30		eqeq1 2827	. . . . . . . . . . . 12 ⊢ (𝑏 = (2^nd ‘𝑞) → (𝑏 = 𝑑 ↔ (2^nd ‘𝑞) = 𝑑))
31		csbeq1 3888	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (2^nd ‘𝑞) → ⦋𝑏 / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷)
32	31	ineq1d 4190	. . . . . . . . . . . . 13 ⊢ (𝑏 = (2^nd ‘𝑞) → (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷))
33	32	eqeq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑏 = (2^nd ‘𝑞) → ((⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅ ↔ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
34	30, 33	orbi12d 915	. . . . . . . . . . 11 ⊢ (𝑏 = (2^nd ‘𝑞) → ((𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) ↔ ((2^nd ‘𝑞) = 𝑑 ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅)))
35		eqeq2 2835	. . . . . . . . . . . 12 ⊢ (𝑑 = (2^nd ‘𝑟) → ((2^nd ‘𝑞) = 𝑑 ↔ (2^nd ‘𝑞) = (2^nd ‘𝑟)))
36		csbeq1 3888	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (2^nd ‘𝑟) → ⦋𝑑 / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷)
37	36	ineq2d 4191	. . . . . . . . . . . . 13 ⊢ (𝑑 = (2^nd ‘𝑟) → (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷))
38	37	eqeq1d 2825	. . . . . . . . . . . 12 ⊢ (𝑑 = (2^nd ‘𝑟) → ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅ ↔ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
39	35, 38	orbi12d 915	. . . . . . . . . . 11 ⊢ (𝑑 = (2^nd ‘𝑟) → (((2^nd ‘𝑞) = 𝑑 ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) ↔ ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
40	34, 39	rspc2v 3635	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑞) ∈ 𝐵 ∧ (2^nd ‘𝑟) ∈ 𝐵) → (∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
41	29, 40	syl5 34	. . . . . . . . 9 ⊢ (((2^nd ‘𝑞) ∈ 𝐵 ∧ (2^nd ‘𝑟) ∈ 𝐵) → (𝜑 → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
42	41	imp 409	. . . . . . . 8 ⊢ ((((2^nd ‘𝑞) ∈ 𝐵 ∧ (2^nd ‘𝑟) ∈ 𝐵) ∧ 𝜑) → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
43	24, 26, 5, 42	syl21anc 835	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
44	22, 43	jca 514	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅) ∧ ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
45		anddi 1007	. . . . . 6 ⊢ ((((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅) ∧ ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)) ↔ ((((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)) ∨ (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))))
46	44, 45	sylib 220	. . . . 5 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)) ∨ (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))))
47		orass 918	. . . . 5 ⊢ (((((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)) ∨ (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))) ↔ (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) ∨ (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))))
48	46, 47	sylib 220	. . . 4 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) ∨ (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))))
49		xpopth 7732	. . . . . . 7 ⊢ ((𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵)) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ↔ 𝑞 = 𝑟))
50	49	adantl 484	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ↔ 𝑞 = 𝑟))
51	50	biimpd 231	. . . . 5 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) → 𝑞 = 𝑟))
52		inss2 4208	. . . . . . . . . 10 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)) ⊆ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)
53		csbin 4393	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) = (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹)
54		csbin 4393	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹) = (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹)
55	53, 54	ineq12i 4189	. . . . . . . . . . 11 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹) ∩ (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹))
56		in4 4204	. . . . . . . . . . 11 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹) ∩ (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹))
57	55, 56	eqtri 2846	. . . . . . . . . 10 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹))
58		vex 3499	. . . . . . . . . . . . 13 ⊢ 𝑞 ∈ V
59		csbnestgw 4375	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ V → ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷)
60	58, 59	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷
61		fvex 6685	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘𝑝) ∈ V
62		disjxpin.2	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (2^nd ‘𝑝) → 𝐷 = 𝐹)
63	61, 62	csbie 3920	. . . . . . . . . . . . 13 ⊢ ⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = 𝐹
64	63	csbeq2i 3893	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋𝑞 / 𝑝⦌𝐹
65		csbfv 6717	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑞)
66		csbeq1 3888	. . . . . . . . . . . . 13 ⊢ (⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑞) → ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷)
67	65, 66	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷
68	60, 64, 67	3eqtr3ri 2855	. . . . . . . . . . 11 ⊢ ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 = ⦋𝑞 / 𝑝⦌𝐹
69		vex 3499	. . . . . . . . . . . . 13 ⊢ 𝑟 ∈ V
70		csbnestgw 4375	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ V → ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷)
71	69, 70	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷
72	63	csbeq2i 3893	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋𝑟 / 𝑝⦌𝐹
73		csbfv 6717	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑟)
74		csbeq1 3888	. . . . . . . . . . . . 13 ⊢ (⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑟) → ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷)
75	73, 74	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷
76	71, 72, 75	3eqtr3ri 2855	. . . . . . . . . . 11 ⊢ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷 = ⦋𝑟 / 𝑝⦌𝐹
77	68, 76	ineq12i 4189	. . . . . . . . . 10 ⊢ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)
78	52, 57, 77	3sstr4i 4012	. . . . . . . . 9 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷)
79		sseq0 4355	. . . . . . . . 9 ⊢ (((⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
80	78, 79	mpan 688	. . . . . . . 8 ⊢ ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
81	80	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
82	81	adantld 493	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
83		inss1 4207	. . . . . . . . . . 11 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)) ⊆ (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸)
84		csbnestgw 4375	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ V → ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶)
85	58, 84	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶
86		fvex 6685	. . . . . . . . . . . . . . 15 ⊢ (1^st ‘𝑝) ∈ V
87		disjxpin.1	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1^st ‘𝑝) → 𝐶 = 𝐸)
88	86, 87	csbie 3920	. . . . . . . . . . . . . 14 ⊢ ⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = 𝐸
89	88	csbeq2i 3893	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋𝑞 / 𝑝⦌𝐸
90		csbfv 6717	. . . . . . . . . . . . . 14 ⊢ ⦋𝑞 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑞)
91		csbeq1 3888	. . . . . . . . . . . . . 14 ⊢ (⦋𝑞 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑞) → ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋(1^st ‘𝑞) / 𝑥⦌𝐶)
92	90, 91	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋(1^st ‘𝑞) / 𝑥⦌𝐶
93	85, 89, 92	3eqtr3ri 2855	. . . . . . . . . . . 12 ⊢ ⦋(1^st ‘𝑞) / 𝑥⦌𝐶 = ⦋𝑞 / 𝑝⦌𝐸
94		csbnestgw 4375	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ V → ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶)
95	69, 94	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶
96	88	csbeq2i 3893	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋𝑟 / 𝑝⦌𝐸
97		csbfv 6717	. . . . . . . . . . . . . 14 ⊢ ⦋𝑟 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑟)
98		csbeq1 3888	. . . . . . . . . . . . . 14 ⊢ (⦋𝑟 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑟) → ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋(1^st ‘𝑟) / 𝑥⦌𝐶)
99	97, 98	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋(1^st ‘𝑟) / 𝑥⦌𝐶
100	95, 96, 99	3eqtr3ri 2855	. . . . . . . . . . . 12 ⊢ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶 = ⦋𝑟 / 𝑝⦌𝐸
101	93, 100	ineq12i 4189	. . . . . . . . . . 11 ⊢ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸)
102	83, 57, 101	3sstr4i 4012	. . . . . . . . . 10 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶)
103		sseq0 4355	. . . . . . . . . 10 ⊢ (((⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) ∧ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
104	102, 103	mpan 688	. . . . . . . . 9 ⊢ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
105	104	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
106	105	adantrd 494	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
107	81	adantld 493	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
108	106, 107	jaod 855	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
109	82, 108	jaod 855	. . . . 5 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) ∨ (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
110	51, 109	orim12d 961	. . . 4 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) ∨ (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))) → (𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)))
111	48, 110	mpd 15	. . 3 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
112	111	ralrimivva 3193	. 2 ⊢ (𝜑 → ∀𝑞 ∈ (𝐴 × 𝐵)∀𝑟 ∈ (𝐴 × 𝐵)(𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
113		disjors 5049	. 2 ⊢ (Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹) ↔ ∀𝑞 ∈ (𝐴 × 𝐵)∀𝑟 ∈ (𝐴 × 𝐵)(𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
114	112, 113	sylibr 236	1 ⊢ (𝜑 → Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 398 ∨ wo 843 = wceq 1537 ∈ wcel 2114 ∀wral 3140 Vcvv 3496 ⦋csb 3885 ∩ cin 3937 ⊆ wss 3938 ∅c0 4293 Disj wdisj 5033 × cxp 5555 ‘cfv 6357 1^st c1st 7689 2^nd c2nd 7690

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2116 ax-9 2124 ax-10 2145 ax-11 2161 ax-12 2177 ax-ext 2795 ax-sep 5205 ax-nul 5212 ax-pow 5268 ax-pr 5332 ax-un 7463

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3an 1085 df-tru 1540 df-fal 1550 df-ex 1781 df-nf 1785 df-sb 2070 df-mo 2622 df-eu 2654 df-clab 2802 df-cleq 2816 df-clel 2895 df-nfc 2965 df-ral 3145 df-rex 3146 df-reu 3147 df-rmo 3148 df-rab 3149 df-v 3498 df-sbc 3775 df-csb 3886 df-dif 3941 df-un 3943 df-in 3945 df-ss 3954 df-nul 4294 df-if 4470 df-sn 4570 df-pr 4572 df-op 4576 df-uni 4841 df-disj 5034 df-br 5069 df-opab 5131 df-mpt 5149 df-id 5462 df-xp 5563 df-rel 5564 df-cnv 5565 df-co 5566 df-dm 5567 df-rn 5568 df-iota 6316 df-fun 6359 df-fv 6365 df-1st 7691 df-2nd 7692

This theorem is referenced by: sibfof 31600

W3C validator