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 28783

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 7089	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝐴 × 𝐵) → (1^st ‘𝑞) ∈ 𝐴)
2	1	ad2antrl 760	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (1^st ‘𝑞) ∈ 𝐴)
3		xp1st 7089	. . . . . . . . 9 ⊢ (𝑟 ∈ (𝐴 × 𝐵) → (1^st ‘𝑟) ∈ 𝐴)
4	3	ad2antll 761	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (1^st ‘𝑟) ∈ 𝐴)
5		simpl 472	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → 𝜑)
6		disjxpin.3	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐶)
7		disjors 4568	. . . . . . . . . . 11 ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
8	6, 7	sylib 207	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
9		eqeq1 2614	. . . . . . . . . . . 12 ⊢ (𝑎 = (1^st ‘𝑞) → (𝑎 = 𝑐 ↔ (1^st ‘𝑞) = 𝑐))
10		csbeq1 3502	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (1^st ‘𝑞) → ⦋𝑎 / 𝑥⦌𝐶 = ⦋(1^st ‘𝑞) / 𝑥⦌𝐶)
11	10	ineq1d 3775	. . . . . . . . . . . . 13 ⊢ (𝑎 = (1^st ‘𝑞) → (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶))
12	11	eqeq1d 2612	. . . . . . . . . . . 12 ⊢ (𝑎 = (1^st ‘𝑞) → ((⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅ ↔ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
13	9, 12	orbi12d 742	. . . . . . . . . . 11 ⊢ (𝑎 = (1^st ‘𝑞) → ((𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) ↔ ((1^st ‘𝑞) = 𝑐 ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅)))
14		eqeq2 2621	. . . . . . . . . . . 12 ⊢ (𝑐 = (1^st ‘𝑟) → ((1^st ‘𝑞) = 𝑐 ↔ (1^st ‘𝑞) = (1^st ‘𝑟)))
15		csbeq1 3502	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (1^st ‘𝑟) → ⦋𝑐 / 𝑥⦌𝐶 = ⦋(1^st ‘𝑟) / 𝑥⦌𝐶)
16	15	ineq2d 3776	. . . . . . . . . . . . 13 ⊢ (𝑐 = (1^st ‘𝑟) → (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶))
17	16	eqeq1d 2612	. . . . . . . . . . . 12 ⊢ (𝑐 = (1^st ‘𝑟) → ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅ ↔ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
18	14, 17	orbi12d 742	. . . . . . . . . . 11 ⊢ (𝑐 = (1^st ‘𝑟) → (((1^st ‘𝑞) = 𝑐 ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) ↔ ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅)))
19	13, 18	rspc2v 3293	. . . . . . . . . 10 ⊢ (((1^st ‘𝑞) ∈ 𝐴 ∧ (1^st ‘𝑟) ∈ 𝐴) → (∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅)))
20	8, 19	syl5 33	. . . . . . . . 9 ⊢ (((1^st ‘𝑞) ∈ 𝐴 ∧ (1^st ‘𝑟) ∈ 𝐴) → (𝜑 → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅)))
21	20	imp 444	. . . . . . . 8 ⊢ ((((1^st ‘𝑞) ∈ 𝐴 ∧ (1^st ‘𝑟) ∈ 𝐴) ∧ 𝜑) → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
22	2, 4, 5, 21	syl21anc 1317	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
23		xp2nd 7090	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝐴 × 𝐵) → (2^nd ‘𝑞) ∈ 𝐵)
24	23	ad2antrl 760	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (2^nd ‘𝑞) ∈ 𝐵)
25		xp2nd 7090	. . . . . . . . 9 ⊢ (𝑟 ∈ (𝐴 × 𝐵) → (2^nd ‘𝑟) ∈ 𝐵)
26	25	ad2antll 761	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (2^nd ‘𝑟) ∈ 𝐵)
27		disjxpin.4	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑦 ∈ 𝐵 𝐷)
28		disjors 4568	. . . . . . . . . . 11 ⊢ (Disj 𝑦 ∈ 𝐵 𝐷 ↔ ∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
29	27, 28	sylib 207	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
30		eqeq1 2614	. . . . . . . . . . . 12 ⊢ (𝑏 = (2^nd ‘𝑞) → (𝑏 = 𝑑 ↔ (2^nd ‘𝑞) = 𝑑))
31		csbeq1 3502	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (2^nd ‘𝑞) → ⦋𝑏 / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷)
32	31	ineq1d 3775	. . . . . . . . . . . . 13 ⊢ (𝑏 = (2^nd ‘𝑞) → (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷))
33	32	eqeq1d 2612	. . . . . . . . . . . 12 ⊢ (𝑏 = (2^nd ‘𝑞) → ((⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅ ↔ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
34	30, 33	orbi12d 742	. . . . . . . . . . 11 ⊢ (𝑏 = (2^nd ‘𝑞) → ((𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) ↔ ((2^nd ‘𝑞) = 𝑑 ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅)))
35		eqeq2 2621	. . . . . . . . . . . 12 ⊢ (𝑑 = (2^nd ‘𝑟) → ((2^nd ‘𝑞) = 𝑑 ↔ (2^nd ‘𝑞) = (2^nd ‘𝑟)))
36		csbeq1 3502	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (2^nd ‘𝑟) → ⦋𝑑 / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷)
37	36	ineq2d 3776	. . . . . . . . . . . . 13 ⊢ (𝑑 = (2^nd ‘𝑟) → (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷))
38	37	eqeq1d 2612	. . . . . . . . . . . 12 ⊢ (𝑑 = (2^nd ‘𝑟) → ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅ ↔ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
39	35, 38	orbi12d 742	. . . . . . . . . . 11 ⊢ (𝑑 = (2^nd ‘𝑟) → (((2^nd ‘𝑞) = 𝑑 ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) ↔ ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
40	34, 39	rspc2v 3293	. . . . . . . . . 10 ⊢ (((2^nd ‘𝑞) ∈ 𝐵 ∧ (2^nd ‘𝑟) ∈ 𝐵) → (∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
41	29, 40	syl5 33	. . . . . . . . 9 ⊢ (((2^nd ‘𝑞) ∈ 𝐵 ∧ (2^nd ‘𝑟) ∈ 𝐵) → (𝜑 → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
42	41	imp 444	. . . . . . . 8 ⊢ ((((2^nd ‘𝑞) ∈ 𝐵 ∧ (2^nd ‘𝑟) ∈ 𝐵) ∧ 𝜑) → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
43	24, 26, 5, 42	syl21anc 1317	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
44	22, 43	jca 553	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅) ∧ ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
45		anddi 910	. . . . . 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 207	. . . . 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 545	. . . . 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 207	. . . 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 7098	. . . . . . 7 ⊢ ((𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵)) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ↔ 𝑞 = 𝑟))
50	49	adantl 481	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ↔ 𝑞 = 𝑟))
51	50	biimpd 218	. . . . 5 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) → 𝑞 = 𝑟))
52		inss2 3796	. . . . . . . . . 10 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)) ⊆ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)
53		csbin 3962	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) = (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹)
54		csbin 3962	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹) = (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹)
55	53, 54	ineq12i 3774	. . . . . . . . . . 11 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹) ∩ (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹))
56		in4 3791	. . . . . . . . . . 11 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹) ∩ (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹))
57	55, 56	eqtri 2632	. . . . . . . . . 10 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹))
58		vex 3176	. . . . . . . . . . . . 13 ⊢ 𝑞 ∈ V
59		csbnestg 3950	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ V → ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷)
60	58, 59	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷
61		fvex 6113	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘𝑝) ∈ V
62		disjxpin.2	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (2^nd ‘𝑝) → 𝐷 = 𝐹)
63	61, 62	csbie 3525	. . . . . . . . . . . . 13 ⊢ ⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = 𝐹
64	63	csbeq2i 3945	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋𝑞 / 𝑝⦌𝐹
65		csbfv 6143	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑞)
66		csbeq1 3502	. . . . . . . . . . . . 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 2641	. . . . . . . . . . 11 ⊢ ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 = ⦋𝑞 / 𝑝⦌𝐹
69		vex 3176	. . . . . . . . . . . . 13 ⊢ 𝑟 ∈ V
70		csbnestg 3950	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ V → ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷)
71	69, 70	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷
72	63	csbeq2i 3945	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋𝑟 / 𝑝⦌𝐹
73		csbfv 6143	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑟)
74		csbeq1 3502	. . . . . . . . . . . . 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 2641	. . . . . . . . . . 11 ⊢ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷 = ⦋𝑟 / 𝑝⦌𝐹
77	68, 76	ineq12i 3774	. . . . . . . . . 10 ⊢ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)
78	52, 57, 77	3sstr4i 3607	. . . . . . . . 9 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷)
79		sseq0 3927	. . . . . . . . 9 ⊢ (((⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
80	78, 79	mpan 702	. . . . . . . 8 ⊢ ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
81	80	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
82	81	adantld 482	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
83		inss1 3795	. . . . . . . . . . 11 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)) ⊆ (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸)
84		csbnestg 3950	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ V → ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶)
85	58, 84	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶
86		fvex 6113	. . . . . . . . . . . . . . 15 ⊢ (1^st ‘𝑝) ∈ V
87		disjxpin.1	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1^st ‘𝑝) → 𝐶 = 𝐸)
88	86, 87	csbie 3525	. . . . . . . . . . . . . 14 ⊢ ⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = 𝐸
89	88	csbeq2i 3945	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋𝑞 / 𝑝⦌𝐸
90		csbfv 6143	. . . . . . . . . . . . . 14 ⊢ ⦋𝑞 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑞)
91		csbeq1 3502	. . . . . . . . . . . . . 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 2641	. . . . . . . . . . . 12 ⊢ ⦋(1^st ‘𝑞) / 𝑥⦌𝐶 = ⦋𝑞 / 𝑝⦌𝐸
94		csbnestg 3950	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ V → ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶)
95	69, 94	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶
96	88	csbeq2i 3945	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋𝑟 / 𝑝⦌𝐸
97		csbfv 6143	. . . . . . . . . . . . . 14 ⊢ ⦋𝑟 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑟)
98		csbeq1 3502	. . . . . . . . . . . . . 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 2641	. . . . . . . . . . . 12 ⊢ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶 = ⦋𝑟 / 𝑝⦌𝐸
101	93, 100	ineq12i 3774	. . . . . . . . . . 11 ⊢ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸)
102	83, 57, 101	3sstr4i 3607	. . . . . . . . . 10 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶)
103		sseq0 3927	. . . . . . . . . 10 ⊢ (((⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) ∧ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
104	102, 103	mpan 702	. . . . . . . . 9 ⊢ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
105	104	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
106	105	adantrd 483	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
107	81	adantld 482	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
108	106, 107	jaod 394	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
109	82, 108	jaod 394	. . . . 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 879	. . . 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 2954	. 2 ⊢ (𝜑 → ∀𝑞 ∈ (𝐴 × 𝐵)∀𝑟 ∈ (𝐴 × 𝐵)(𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
113		disjors 4568	. 2 ⊢ (Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹) ↔ ∀𝑞 ∈ (𝐴 × 𝐵)∀𝑟 ∈ (𝐴 × 𝐵)(𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
114	112, 113	sylibr 223	1 ⊢ (𝜑 → Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∨ wo 382 ∧ wa 383 = wceq 1475 ∈ wcel 1977 ∀wral 2896 Vcvv 3173 ⦋csb 3499 ∩ cin 3539 ⊆ wss 3540 ∅c0 3874 Disj wdisj 4553 × cxp 5036 ‘cfv 5804 1^st c1st 7057 2^nd c2nd 7058

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-8 1979 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pow 4769 ax-pr 4833 ax-un 6847

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-fal 1481 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-reu 2903 df-rmo 2904 df-rab 2905 df-v 3175 df-sbc 3403 df-csb 3500 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-uni 4373 df-disj 4554 df-br 4584 df-opab 4644 df-mpt 4645 df-id 4953 df-xp 5044 df-rel 5045 df-cnv 5046 df-co 5047 df-dm 5048 df-rn 5049 df-iota 5768 df-fun 5806 df-fv 5812 df-1st 7059 df-2nd 7060

This theorem is referenced by: sibfof 29729

W3C validator