disjxpin

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

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

Proof

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

Metamath Proof Explorer

Theorem disjxpin

Proof