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 32610

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 8062	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝐴 × 𝐵) → (1^st ‘𝑞) ∈ 𝐴)
2	1	ad2antrl 727	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (1^st ‘𝑞) ∈ 𝐴)
3		xp1st 8062	. . . . . . . . 9 ⊢ (𝑟 ∈ (𝐴 × 𝐵) → (1^st ‘𝑟) ∈ 𝐴)
4	3	ad2antll 728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (1^st ‘𝑟) ∈ 𝐴)
5		simpl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → 𝜑)
6		disjxpin.3	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐶)
7		disjors 5149	. . . . . . . . . . 11 ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
8	6, 7	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
9		eqeq1 2744	. . . . . . . . . . . 12 ⊢ (𝑎 = (1^st ‘𝑞) → (𝑎 = 𝑐 ↔ (1^st ‘𝑞) = 𝑐))
10		csbeq1 3924	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (1^st ‘𝑞) → ⦋𝑎 / 𝑥⦌𝐶 = ⦋(1^st ‘𝑞) / 𝑥⦌𝐶)
11	10	ineq1d 4240	. . . . . . . . . . . . 13 ⊢ (𝑎 = (1^st ‘𝑞) → (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶))
12	11	eqeq1d 2742	. . . . . . . . . . . 12 ⊢ (𝑎 = (1^st ‘𝑞) → ((⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅ ↔ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
13	9, 12	orbi12d 917	. . . . . . . . . . 11 ⊢ (𝑎 = (1^st ‘𝑞) → ((𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) ↔ ((1^st ‘𝑞) = 𝑐 ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅)))
14		eqeq2 2752	. . . . . . . . . . . 12 ⊢ (𝑐 = (1^st ‘𝑟) → ((1^st ‘𝑞) = 𝑐 ↔ (1^st ‘𝑞) = (1^st ‘𝑟)))
15		csbeq1 3924	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (1^st ‘𝑟) → ⦋𝑐 / 𝑥⦌𝐶 = ⦋(1^st ‘𝑟) / 𝑥⦌𝐶)
16	15	ineq2d 4241	. . . . . . . . . . . . 13 ⊢ (𝑐 = (1^st ‘𝑟) → (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶))
17	16	eqeq1d 2742	. . . . . . . . . . . 12 ⊢ (𝑐 = (1^st ‘𝑟) → ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅ ↔ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
18	14, 17	orbi12d 917	. . . . . . . . . . 11 ⊢ (𝑐 = (1^st ‘𝑟) → (((1^st ‘𝑞) = 𝑐 ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) ↔ ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅)))
19	13, 18	rspc2v 3646	. . . . . . . . . 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 406	. . . . . . . 8 ⊢ ((((1^st ‘𝑞) ∈ 𝐴 ∧ (1^st ‘𝑟) ∈ 𝐴) ∧ 𝜑) → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
22	2, 4, 5, 21	syl21anc 837	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
23		xp2nd 8063	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝐴 × 𝐵) → (2^nd ‘𝑞) ∈ 𝐵)
24	23	ad2antrl 727	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (2^nd ‘𝑞) ∈ 𝐵)
25		xp2nd 8063	. . . . . . . . 9 ⊢ (𝑟 ∈ (𝐴 × 𝐵) → (2^nd ‘𝑟) ∈ 𝐵)
26	25	ad2antll 728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (2^nd ‘𝑟) ∈ 𝐵)
27		disjxpin.4	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑦 ∈ 𝐵 𝐷)
28		disjors 5149	. . . . . . . . . . 11 ⊢ (Disj 𝑦 ∈ 𝐵 𝐷 ↔ ∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
29	27, 28	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
30		eqeq1 2744	. . . . . . . . . . . 12 ⊢ (𝑏 = (2^nd ‘𝑞) → (𝑏 = 𝑑 ↔ (2^nd ‘𝑞) = 𝑑))
31		csbeq1 3924	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (2^nd ‘𝑞) → ⦋𝑏 / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷)
32	31	ineq1d 4240	. . . . . . . . . . . . 13 ⊢ (𝑏 = (2^nd ‘𝑞) → (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷))
33	32	eqeq1d 2742	. . . . . . . . . . . 12 ⊢ (𝑏 = (2^nd ‘𝑞) → ((⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅ ↔ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
34	30, 33	orbi12d 917	. . . . . . . . . . 11 ⊢ (𝑏 = (2^nd ‘𝑞) → ((𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) ↔ ((2^nd ‘𝑞) = 𝑑 ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅)))
35		eqeq2 2752	. . . . . . . . . . . 12 ⊢ (𝑑 = (2^nd ‘𝑟) → ((2^nd ‘𝑞) = 𝑑 ↔ (2^nd ‘𝑞) = (2^nd ‘𝑟)))
36		csbeq1 3924	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (2^nd ‘𝑟) → ⦋𝑑 / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷)
37	36	ineq2d 4241	. . . . . . . . . . . . 13 ⊢ (𝑑 = (2^nd ‘𝑟) → (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷))
38	37	eqeq1d 2742	. . . . . . . . . . . 12 ⊢ (𝑑 = (2^nd ‘𝑟) → ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅ ↔ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
39	35, 38	orbi12d 917	. . . . . . . . . . 11 ⊢ (𝑑 = (2^nd ‘𝑟) → (((2^nd ‘𝑞) = 𝑑 ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) ↔ ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
40	34, 39	rspc2v 3646	. . . . . . . . . 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 406	. . . . . . . 8 ⊢ ((((2^nd ‘𝑞) ∈ 𝐵 ∧ (2^nd ‘𝑟) ∈ 𝐵) ∧ 𝜑) → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
43	24, 26, 5, 42	syl21anc 837	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
44	22, 43	jca 511	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅) ∧ ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
45		anddi 1011	. . . . . 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 218	. . . . 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 920	. . . . 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 218	. . . 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 8071	. . . . . . 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 229	. . . . 5 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) → 𝑞 = 𝑟))
52		inss2 4259	. . . . . . . . . 10 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)) ⊆ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)
53		csbin 4465	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) = (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹)
54		csbin 4465	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹) = (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹)
55	53, 54	ineq12i 4239	. . . . . . . . . . 11 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹) ∩ (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹))
56		in4 4255	. . . . . . . . . . 11 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹) ∩ (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹))
57	55, 56	eqtri 2768	. . . . . . . . . 10 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹))
58		vex 3492	. . . . . . . . . . . . 13 ⊢ 𝑞 ∈ V
59		csbnestgw 4447	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ V → ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷)
60	58, 59	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷
61		fvex 6933	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘𝑝) ∈ V
62		disjxpin.2	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (2^nd ‘𝑝) → 𝐷 = 𝐹)
63	61, 62	csbie 3957	. . . . . . . . . . . . 13 ⊢ ⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = 𝐹
64	63	csbeq2i 3929	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋𝑞 / 𝑝⦌𝐹
65		csbfv 6970	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑞)
66		csbeq1 3924	. . . . . . . . . . . . 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 2777	. . . . . . . . . . 11 ⊢ ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 = ⦋𝑞 / 𝑝⦌𝐹
69		vex 3492	. . . . . . . . . . . . 13 ⊢ 𝑟 ∈ V
70		csbnestgw 4447	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ V → ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷)
71	69, 70	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷
72	63	csbeq2i 3929	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋𝑟 / 𝑝⦌𝐹
73		csbfv 6970	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑟)
74		csbeq1 3924	. . . . . . . . . . . . 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 2777	. . . . . . . . . . 11 ⊢ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷 = ⦋𝑟 / 𝑝⦌𝐹
77	68, 76	ineq12i 4239	. . . . . . . . . 10 ⊢ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)
78	52, 57, 77	3sstr4i 4052	. . . . . . . . 9 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷)
79		sseq0 4426	. . . . . . . . 9 ⊢ (((⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
80	78, 79	mpan 689	. . . . . . . 8 ⊢ ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
81	80	a1i 11	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
82	81	adantld 490	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((1^st ‘𝑞) = (1^st ‘𝑟) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
83		inss1 4258	. . . . . . . . . . 11 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)) ⊆ (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸)
84		csbnestgw 4447	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ V → ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶)
85	58, 84	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶
86		fvex 6933	. . . . . . . . . . . . . . 15 ⊢ (1^st ‘𝑝) ∈ V
87		disjxpin.1	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1^st ‘𝑝) → 𝐶 = 𝐸)
88	86, 87	csbie 3957	. . . . . . . . . . . . . 14 ⊢ ⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = 𝐸
89	88	csbeq2i 3929	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋𝑞 / 𝑝⦌𝐸
90		csbfv 6970	. . . . . . . . . . . . . 14 ⊢ ⦋𝑞 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑞)
91		csbeq1 3924	. . . . . . . . . . . . . 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 2777	. . . . . . . . . . . 12 ⊢ ⦋(1^st ‘𝑞) / 𝑥⦌𝐶 = ⦋𝑞 / 𝑝⦌𝐸
94		csbnestgw 4447	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ V → ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶)
95	69, 94	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶
96	88	csbeq2i 3929	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋𝑟 / 𝑝⦌𝐸
97		csbfv 6970	. . . . . . . . . . . . . 14 ⊢ ⦋𝑟 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑟)
98		csbeq1 3924	. . . . . . . . . . . . . 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 2777	. . . . . . . . . . . 12 ⊢ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶 = ⦋𝑟 / 𝑝⦌𝐸
101	93, 100	ineq12i 4239	. . . . . . . . . . 11 ⊢ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸)
102	83, 57, 101	3sstr4i 4052	. . . . . . . . . 10 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶)
103		sseq0 4426	. . . . . . . . . 10 ⊢ (((⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) ∧ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
104	102, 103	mpan 689	. . . . . . . . 9 ⊢ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
105	104	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
106	105	adantrd 491	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
107	81	adantld 490	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
108	106, 107	jaod 858	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
109	82, 108	jaod 858	. . . . 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 965	. . . 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 3208	. 2 ⊢ (𝜑 → ∀𝑞 ∈ (𝐴 × 𝐵)∀𝑟 ∈ (𝐴 × 𝐵)(𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
113		disjors 5149	. 2 ⊢ (Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹) ↔ ∀𝑞 ∈ (𝐴 × 𝐵)∀𝑟 ∈ (𝐴 × 𝐵)(𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
114	112, 113	sylibr 234	1 ⊢ (𝜑 → Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 846 = wceq 1537 ∈ wcel 2108 ∀wral 3067 Vcvv 3488 ⦋csb 3921 ∩ cin 3975 ⊆ wss 3976 ∅c0 4352 Disj wdisj 5133 × cxp 5698 ‘cfv 6573 1^st c1st 8028 2^nd c2nd 8029

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-sep 5317 ax-nul 5324 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rmo 3388 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-nul 4353 df-if 4549 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-disj 5134 df-br 5167 df-opab 5229 df-mpt 5250 df-id 5593 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-iota 6525 df-fun 6575 df-fv 6581 df-1st 8030 df-2nd 8031

This theorem is referenced by: sibfof 34305

W3C validator