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 29401

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 7198	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝐴 × 𝐵) → (1^st ‘𝑞) ∈ 𝐴)
2	1	ad2antrl 764	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (1^st ‘𝑞) ∈ 𝐴)
3		xp1st 7198	. . . . . . . . 9 ⊢ (𝑟 ∈ (𝐴 × 𝐵) → (1^st ‘𝑟) ∈ 𝐴)
4	3	ad2antll 765	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (1^st ‘𝑟) ∈ 𝐴)
5		simpl 473	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → 𝜑)
6		disjxpin.3	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐶)
7		disjors 4635	. . . . . . . . . . 11 ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
8	6, 7	sylib 208	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
9		eqeq1 2626	. . . . . . . . . . . 12 ⊢ (𝑎 = (1^st ‘𝑞) → (𝑎 = 𝑐 ↔ (1^st ‘𝑞) = 𝑐))
10		csbeq1 3536	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (1^st ‘𝑞) → ⦋𝑎 / 𝑥⦌𝐶 = ⦋(1^st ‘𝑞) / 𝑥⦌𝐶)
11	10	ineq1d 3813	. . . . . . . . . . . . 13 ⊢ (𝑎 = (1^st ‘𝑞) → (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶))
12	11	eqeq1d 2624	. . . . . . . . . . . 12 ⊢ (𝑎 = (1^st ‘𝑞) → ((⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅ ↔ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
13	9, 12	orbi12d 746	. . . . . . . . . . 11 ⊢ (𝑎 = (1^st ‘𝑞) → ((𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) ↔ ((1^st ‘𝑞) = 𝑐 ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅)))
14		eqeq2 2633	. . . . . . . . . . . 12 ⊢ (𝑐 = (1^st ‘𝑟) → ((1^st ‘𝑞) = 𝑐 ↔ (1^st ‘𝑞) = (1^st ‘𝑟)))
15		csbeq1 3536	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (1^st ‘𝑟) → ⦋𝑐 / 𝑥⦌𝐶 = ⦋(1^st ‘𝑟) / 𝑥⦌𝐶)
16	15	ineq2d 3814	. . . . . . . . . . . . 13 ⊢ (𝑐 = (1^st ‘𝑟) → (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶))
17	16	eqeq1d 2624	. . . . . . . . . . . 12 ⊢ (𝑐 = (1^st ‘𝑟) → ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅ ↔ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
18	14, 17	orbi12d 746	. . . . . . . . . . 11 ⊢ (𝑐 = (1^st ‘𝑟) → (((1^st ‘𝑞) = 𝑐 ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) ↔ ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅)))
19	13, 18	rspc2v 3322	. . . . . . . . . 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 445	. . . . . . . 8 ⊢ ((((1^st ‘𝑞) ∈ 𝐴 ∧ (1^st ‘𝑟) ∈ 𝐴) ∧ 𝜑) → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
22	2, 4, 5, 21	syl21anc 1325	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
23		xp2nd 7199	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝐴 × 𝐵) → (2^nd ‘𝑞) ∈ 𝐵)
24	23	ad2antrl 764	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (2^nd ‘𝑞) ∈ 𝐵)
25		xp2nd 7199	. . . . . . . . 9 ⊢ (𝑟 ∈ (𝐴 × 𝐵) → (2^nd ‘𝑟) ∈ 𝐵)
26	25	ad2antll 765	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (2^nd ‘𝑟) ∈ 𝐵)
27		disjxpin.4	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑦 ∈ 𝐵 𝐷)
28		disjors 4635	. . . . . . . . . . 11 ⊢ (Disj 𝑦 ∈ 𝐵 𝐷 ↔ ∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
29	27, 28	sylib 208	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
30		eqeq1 2626	. . . . . . . . . . . 12 ⊢ (𝑏 = (2^nd ‘𝑞) → (𝑏 = 𝑑 ↔ (2^nd ‘𝑞) = 𝑑))
31		csbeq1 3536	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (2^nd ‘𝑞) → ⦋𝑏 / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷)
32	31	ineq1d 3813	. . . . . . . . . . . . 13 ⊢ (𝑏 = (2^nd ‘𝑞) → (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷))
33	32	eqeq1d 2624	. . . . . . . . . . . 12 ⊢ (𝑏 = (2^nd ‘𝑞) → ((⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅ ↔ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
34	30, 33	orbi12d 746	. . . . . . . . . . 11 ⊢ (𝑏 = (2^nd ‘𝑞) → ((𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) ↔ ((2^nd ‘𝑞) = 𝑑 ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅)))
35		eqeq2 2633	. . . . . . . . . . . 12 ⊢ (𝑑 = (2^nd ‘𝑟) → ((2^nd ‘𝑞) = 𝑑 ↔ (2^nd ‘𝑞) = (2^nd ‘𝑟)))
36		csbeq1 3536	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (2^nd ‘𝑟) → ⦋𝑑 / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷)
37	36	ineq2d 3814	. . . . . . . . . . . . 13 ⊢ (𝑑 = (2^nd ‘𝑟) → (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷))
38	37	eqeq1d 2624	. . . . . . . . . . . 12 ⊢ (𝑑 = (2^nd ‘𝑟) → ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅ ↔ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
39	35, 38	orbi12d 746	. . . . . . . . . . 11 ⊢ (𝑑 = (2^nd ‘𝑟) → (((2^nd ‘𝑞) = 𝑑 ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) ↔ ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
40	34, 39	rspc2v 3322	. . . . . . . . . 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 445	. . . . . . . 8 ⊢ ((((2^nd ‘𝑞) ∈ 𝐵 ∧ (2^nd ‘𝑟) ∈ 𝐵) ∧ 𝜑) → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
43	24, 26, 5, 42	syl21anc 1325	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
44	22, 43	jca 554	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅) ∧ ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
45		anddi 914	. . . . . 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 208	. . . . 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 546	. . . . 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 208	. . . 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 7207	. . . . . . 7 ⊢ ((𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵)) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ↔ 𝑞 = 𝑟))
50	49	adantl 482	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ↔ 𝑞 = 𝑟))
51	50	biimpd 219	. . . . 5 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) → 𝑞 = 𝑟))
52		inss2 3834	. . . . . . . . . 10 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)) ⊆ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)
53		csbin 4010	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) = (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹)
54		csbin 4010	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹) = (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹)
55	53, 54	ineq12i 3812	. . . . . . . . . . 11 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹) ∩ (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹))
56		in4 3829	. . . . . . . . . . 11 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹) ∩ (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹))
57	55, 56	eqtri 2644	. . . . . . . . . 10 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹))
58		vex 3203	. . . . . . . . . . . . 13 ⊢ 𝑞 ∈ V
59		csbnestg 3998	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ V → ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷)
60	58, 59	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷
61		fvex 6201	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘𝑝) ∈ V
62		disjxpin.2	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (2^nd ‘𝑝) → 𝐷 = 𝐹)
63	61, 62	csbie 3559	. . . . . . . . . . . . 13 ⊢ ⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = 𝐹
64	63	csbeq2i 3993	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋𝑞 / 𝑝⦌𝐹
65		csbfv 6233	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑞)
66		csbeq1 3536	. . . . . . . . . . . . 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 2653	. . . . . . . . . . 11 ⊢ ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 = ⦋𝑞 / 𝑝⦌𝐹
69		vex 3203	. . . . . . . . . . . . 13 ⊢ 𝑟 ∈ V
70		csbnestg 3998	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ V → ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷)
71	69, 70	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷
72	63	csbeq2i 3993	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋𝑟 / 𝑝⦌𝐹
73		csbfv 6233	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑟)
74		csbeq1 3536	. . . . . . . . . . . . 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 2653	. . . . . . . . . . 11 ⊢ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷 = ⦋𝑟 / 𝑝⦌𝐹
77	68, 76	ineq12i 3812	. . . . . . . . . 10 ⊢ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)
78	52, 57, 77	3sstr4i 3644	. . . . . . . . 9 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷)
79		sseq0 3975	. . . . . . . . 9 ⊢ (((⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
80	78, 79	mpan 706	. . . . . . . 8 ⊢ ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
81	80	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
82	81	adantld 483	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
83		inss1 3833	. . . . . . . . . . 11 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)) ⊆ (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸)
84		csbnestg 3998	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ V → ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶)
85	58, 84	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶
86		fvex 6201	. . . . . . . . . . . . . . 15 ⊢ (1^st ‘𝑝) ∈ V
87		disjxpin.1	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1^st ‘𝑝) → 𝐶 = 𝐸)
88	86, 87	csbie 3559	. . . . . . . . . . . . . 14 ⊢ ⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = 𝐸
89	88	csbeq2i 3993	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋𝑞 / 𝑝⦌𝐸
90		csbfv 6233	. . . . . . . . . . . . . 14 ⊢ ⦋𝑞 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑞)
91		csbeq1 3536	. . . . . . . . . . . . . 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 2653	. . . . . . . . . . . 12 ⊢ ⦋(1^st ‘𝑞) / 𝑥⦌𝐶 = ⦋𝑞 / 𝑝⦌𝐸
94		csbnestg 3998	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ V → ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶)
95	69, 94	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶
96	88	csbeq2i 3993	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋𝑟 / 𝑝⦌𝐸
97		csbfv 6233	. . . . . . . . . . . . . 14 ⊢ ⦋𝑟 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑟)
98		csbeq1 3536	. . . . . . . . . . . . . 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 2653	. . . . . . . . . . . 12 ⊢ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶 = ⦋𝑟 / 𝑝⦌𝐸
101	93, 100	ineq12i 3812	. . . . . . . . . . 11 ⊢ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸)
102	83, 57, 101	3sstr4i 3644	. . . . . . . . . 10 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶)
103		sseq0 3975	. . . . . . . . . 10 ⊢ (((⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) ∧ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
104	102, 103	mpan 706	. . . . . . . . 9 ⊢ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
105	104	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
106	105	adantrd 484	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
107	81	adantld 483	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
108	106, 107	jaod 395	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
109	82, 108	jaod 395	. . . . 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 883	. . . 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 2971	. 2 ⊢ (𝜑 → ∀𝑞 ∈ (𝐴 × 𝐵)∀𝑟 ∈ (𝐴 × 𝐵)(𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
113		disjors 4635	. 2 ⊢ (Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹) ↔ ∀𝑞 ∈ (𝐴 × 𝐵)∀𝑟 ∈ (𝐴 × 𝐵)(𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
114	112, 113	sylibr 224	1 ⊢ (𝜑 → Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∨ wo 383 ∧ wa 384 = wceq 1483 ∈ wcel 1990 ∀wral 2912 Vcvv 3200 ⦋csb 3533 ∩ cin 3573 ⊆ wss 3574 ∅c0 3915 Disj wdisj 4620 × cxp 5112 ‘cfv 5888 1^st c1st 7166 2^nd c2nd 7167

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-iota 5851 df-fun 5890 df-fv 5896 df-1st 7168 df-2nd 7169

This theorem is referenced by: sibfof 30402

W3C validator