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 32601

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 8046	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝐴 × 𝐵) → (1^st ‘𝑞) ∈ 𝐴)
2	1	ad2antrl 728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (1^st ‘𝑞) ∈ 𝐴)
3		xp1st 8046	. . . . . . . . 9 ⊢ (𝑟 ∈ (𝐴 × 𝐵) → (1^st ‘𝑟) ∈ 𝐴)
4	3	ad2antll 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (1^st ‘𝑟) ∈ 𝐴)
5		simpl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → 𝜑)
6		disjxpin.3	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐶)
7		disjors 5126	. . . . . . . . . . 11 ⊢ (Disj 𝑥 ∈ 𝐴 𝐶 ↔ ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
8	6, 7	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑎 ∈ 𝐴 ∀𝑐 ∈ 𝐴 (𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
9		eqeq1 2741	. . . . . . . . . . . 12 ⊢ (𝑎 = (1^st ‘𝑞) → (𝑎 = 𝑐 ↔ (1^st ‘𝑞) = 𝑐))
10		csbeq1 3902	. . . . . . . . . . . . . 14 ⊢ (𝑎 = (1^st ‘𝑞) → ⦋𝑎 / 𝑥⦌𝐶 = ⦋(1^st ‘𝑞) / 𝑥⦌𝐶)
11	10	ineq1d 4219	. . . . . . . . . . . . 13 ⊢ (𝑎 = (1^st ‘𝑞) → (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶))
12	11	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑎 = (1^st ‘𝑞) → ((⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅ ↔ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅))
13	9, 12	orbi12d 919	. . . . . . . . . . 11 ⊢ (𝑎 = (1^st ‘𝑞) → ((𝑎 = 𝑐 ∨ (⦋𝑎 / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) ↔ ((1^st ‘𝑞) = 𝑐 ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅)))
14		eqeq2 2749	. . . . . . . . . . . 12 ⊢ (𝑐 = (1^st ‘𝑟) → ((1^st ‘𝑞) = 𝑐 ↔ (1^st ‘𝑞) = (1^st ‘𝑟)))
15		csbeq1 3902	. . . . . . . . . . . . . 14 ⊢ (𝑐 = (1^st ‘𝑟) → ⦋𝑐 / 𝑥⦌𝐶 = ⦋(1^st ‘𝑟) / 𝑥⦌𝐶)
16	15	ineq2d 4220	. . . . . . . . . . . . 13 ⊢ (𝑐 = (1^st ‘𝑟) → (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶))
17	16	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑐 = (1^st ‘𝑟) → ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅ ↔ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
18	14, 17	orbi12d 919	. . . . . . . . . . 11 ⊢ (𝑐 = (1^st ‘𝑟) → (((1^st ‘𝑞) = 𝑐 ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋𝑐 / 𝑥⦌𝐶) = ∅) ↔ ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅)))
19	13, 18	rspc2v 3633	. . . . . . . . . 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 838	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((1^st ‘𝑞) = (1^st ‘𝑟) ∨ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅))
23		xp2nd 8047	. . . . . . . . 9 ⊢ (𝑞 ∈ (𝐴 × 𝐵) → (2^nd ‘𝑞) ∈ 𝐵)
24	23	ad2antrl 728	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (2^nd ‘𝑞) ∈ 𝐵)
25		xp2nd 8047	. . . . . . . . 9 ⊢ (𝑟 ∈ (𝐴 × 𝐵) → (2^nd ‘𝑟) ∈ 𝐵)
26	25	ad2antll 729	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → (2^nd ‘𝑟) ∈ 𝐵)
27		disjxpin.4	. . . . . . . . . . 11 ⊢ (𝜑 → Disj 𝑦 ∈ 𝐵 𝐷)
28		disjors 5126	. . . . . . . . . . 11 ⊢ (Disj 𝑦 ∈ 𝐵 𝐷 ↔ ∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
29	27, 28	sylib 218	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑏 ∈ 𝐵 ∀𝑑 ∈ 𝐵 (𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
30		eqeq1 2741	. . . . . . . . . . . 12 ⊢ (𝑏 = (2^nd ‘𝑞) → (𝑏 = 𝑑 ↔ (2^nd ‘𝑞) = 𝑑))
31		csbeq1 3902	. . . . . . . . . . . . . 14 ⊢ (𝑏 = (2^nd ‘𝑞) → ⦋𝑏 / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷)
32	31	ineq1d 4219	. . . . . . . . . . . . 13 ⊢ (𝑏 = (2^nd ‘𝑞) → (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷))
33	32	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑏 = (2^nd ‘𝑞) → ((⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅ ↔ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅))
34	30, 33	orbi12d 919	. . . . . . . . . . 11 ⊢ (𝑏 = (2^nd ‘𝑞) → ((𝑏 = 𝑑 ∨ (⦋𝑏 / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) ↔ ((2^nd ‘𝑞) = 𝑑 ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅)))
35		eqeq2 2749	. . . . . . . . . . . 12 ⊢ (𝑑 = (2^nd ‘𝑟) → ((2^nd ‘𝑞) = 𝑑 ↔ (2^nd ‘𝑞) = (2^nd ‘𝑟)))
36		csbeq1 3902	. . . . . . . . . . . . . 14 ⊢ (𝑑 = (2^nd ‘𝑟) → ⦋𝑑 / 𝑦⦌𝐷 = ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷)
37	36	ineq2d 4220	. . . . . . . . . . . . 13 ⊢ (𝑑 = (2^nd ‘𝑟) → (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷))
38	37	eqeq1d 2739	. . . . . . . . . . . 12 ⊢ (𝑑 = (2^nd ‘𝑟) → ((⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅ ↔ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅))
39	35, 38	orbi12d 919	. . . . . . . . . . 11 ⊢ (𝑑 = (2^nd ‘𝑟) → (((2^nd ‘𝑞) = 𝑑 ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋𝑑 / 𝑦⦌𝐷) = ∅) ↔ ((2^nd ‘𝑞) = (2^nd ‘𝑟) ∨ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)))
40	34, 39	rspc2v 3633	. . . . . . . . . 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 838	. . . . . . 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 1013	. . . . . 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 922	. . . . 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 8055	. . . . . . 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 4238	. . . . . . . . . 10 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)) ⊆ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)
53		csbin 4442	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) = (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹)
54		csbin 4442	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹) = (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹)
55	53, 54	ineq12i 4218	. . . . . . . . . . 11 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹) ∩ (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹))
56		in4 4234	. . . . . . . . . . 11 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑞 / 𝑝⦌𝐹) ∩ (⦋𝑟 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹))
57	55, 56	eqtri 2765	. . . . . . . . . 10 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹))
58		vex 3484	. . . . . . . . . . . . 13 ⊢ 𝑞 ∈ V
59		csbnestgw 4424	. . . . . . . . . . . . 13 ⊢ (𝑞 ∈ V → ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷)
60	58, 59	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷
61		fvex 6919	. . . . . . . . . . . . . 14 ⊢ (2^nd ‘𝑝) ∈ V
62		disjxpin.2	. . . . . . . . . . . . . 14 ⊢ (𝑦 = (2^nd ‘𝑝) → 𝐷 = 𝐹)
63	61, 62	csbie 3934	. . . . . . . . . . . . 13 ⊢ ⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = 𝐹
64	63	csbeq2i 3907	. . . . . . . . . . . 12 ⊢ ⦋𝑞 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋𝑞 / 𝑝⦌𝐹
65		csbfv 6956	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑞)
66		csbeq1 3902	. . . . . . . . . . . . 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 2774	. . . . . . . . . . 11 ⊢ ⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 = ⦋𝑞 / 𝑝⦌𝐹
69		vex 3484	. . . . . . . . . . . . 13 ⊢ 𝑟 ∈ V
70		csbnestgw 4424	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ V → ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷)
71	69, 70	ax-mp 5	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) / 𝑦⦌𝐷
72	63	csbeq2i 3907	. . . . . . . . . . . 12 ⊢ ⦋𝑟 / 𝑝⦌⦋(2^nd ‘𝑝) / 𝑦⦌𝐷 = ⦋𝑟 / 𝑝⦌𝐹
73		csbfv 6956	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌(2^nd ‘𝑝) = (2^nd ‘𝑟)
74		csbeq1 3902	. . . . . . . . . . . . 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 2774	. . . . . . . . . . 11 ⊢ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷 = ⦋𝑟 / 𝑝⦌𝐹
77	68, 76	ineq12i 4218	. . . . . . . . . 10 ⊢ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)
78	52, 57, 77	3sstr4i 4035	. . . . . . . . 9 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷)
79		sseq0 4403	. . . . . . . . 9 ⊢ (((⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
80	78, 79	mpan 690	. . . . . . . 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 4237	. . . . . . . . . . 11 ⊢ ((⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸) ∩ (⦋𝑞 / 𝑝⦌𝐹 ∩ ⦋𝑟 / 𝑝⦌𝐹)) ⊆ (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸)
84		csbnestgw 4424	. . . . . . . . . . . . . 14 ⊢ (𝑞 ∈ V → ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶)
85	58, 84	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑞 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶
86		fvex 6919	. . . . . . . . . . . . . . 15 ⊢ (1^st ‘𝑝) ∈ V
87		disjxpin.1	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = (1^st ‘𝑝) → 𝐶 = 𝐸)
88	86, 87	csbie 3934	. . . . . . . . . . . . . 14 ⊢ ⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = 𝐸
89	88	csbeq2i 3907	. . . . . . . . . . . . 13 ⊢ ⦋𝑞 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋𝑞 / 𝑝⦌𝐸
90		csbfv 6956	. . . . . . . . . . . . . 14 ⊢ ⦋𝑞 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑞)
91		csbeq1 3902	. . . . . . . . . . . . . 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 2774	. . . . . . . . . . . 12 ⊢ ⦋(1^st ‘𝑞) / 𝑥⦌𝐶 = ⦋𝑞 / 𝑝⦌𝐸
94		csbnestgw 4424	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ V → ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶)
95	69, 94	ax-mp 5	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋⦋𝑟 / 𝑝⦌(1^st ‘𝑝) / 𝑥⦌𝐶
96	88	csbeq2i 3907	. . . . . . . . . . . . 13 ⊢ ⦋𝑟 / 𝑝⦌⦋(1^st ‘𝑝) / 𝑥⦌𝐶 = ⦋𝑟 / 𝑝⦌𝐸
97		csbfv 6956	. . . . . . . . . . . . . 14 ⊢ ⦋𝑟 / 𝑝⦌(1^st ‘𝑝) = (1^st ‘𝑟)
98		csbeq1 3902	. . . . . . . . . . . . . 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 2774	. . . . . . . . . . . 12 ⊢ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶 = ⦋𝑟 / 𝑝⦌𝐸
101	93, 100	ineq12i 4218	. . . . . . . . . . 11 ⊢ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = (⦋𝑞 / 𝑝⦌𝐸 ∩ ⦋𝑟 / 𝑝⦌𝐸)
102	83, 57, 101	3sstr4i 4035	. . . . . . . . . 10 ⊢ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶)
103		sseq0 4403	. . . . . . . . . 10 ⊢ (((⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) ⊆ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) ∧ (⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅)
104	102, 103	mpan 690	. . . . . . . . 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 860	. . . . . 6 ⊢ ((𝜑 ∧ (𝑞 ∈ (𝐴 × 𝐵) ∧ 𝑟 ∈ (𝐴 × 𝐵))) → ((((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (2^nd ‘𝑞) = (2^nd ‘𝑟)) ∨ ((⦋(1^st ‘𝑞) / 𝑥⦌𝐶 ∩ ⦋(1^st ‘𝑟) / 𝑥⦌𝐶) = ∅ ∧ (⦋(2^nd ‘𝑞) / 𝑦⦌𝐷 ∩ ⦋(2^nd ‘𝑟) / 𝑦⦌𝐷) = ∅)) → (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
109	82, 108	jaod 860	. . . . 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 967	. . . 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 3202	. 2 ⊢ (𝜑 → ∀𝑞 ∈ (𝐴 × 𝐵)∀𝑟 ∈ (𝐴 × 𝐵)(𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
113		disjors 5126	. 2 ⊢ (Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹) ↔ ∀𝑞 ∈ (𝐴 × 𝐵)∀𝑟 ∈ (𝐴 × 𝐵)(𝑞 = 𝑟 ∨ (⦋𝑞 / 𝑝⦌(𝐸 ∩ 𝐹) ∩ ⦋𝑟 / 𝑝⦌(𝐸 ∩ 𝐹)) = ∅))
114	112, 113	sylibr 234	1 ⊢ (𝜑 → Disj 𝑝 ∈ (𝐴 × 𝐵)(𝐸 ∩ 𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 848 = wceq 1540 ∈ wcel 2108 ∀wral 3061 Vcvv 3480 ⦋csb 3899 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 Disj wdisj 5110 × cxp 5683 ‘cfv 6561 1^st c1st 8012 2^nd c2nd 8013

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-sep 5296 ax-nul 5306 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3380 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-nul 4334 df-if 4526 df-sn 4627 df-pr 4629 df-op 4633 df-uni 4908 df-disj 5111 df-br 5144 df-opab 5206 df-mpt 5226 df-id 5578 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-iota 6514 df-fun 6563 df-fv 6569 df-1st 8014 df-2nd 8015

This theorem is referenced by: sibfof 34342

W3C validator