Theorem inxpxrn

Description: Two ways to express the intersection of a range Cartesian product with a Cartesian product. (Contributed by Peter Mazsa, 10-Apr-2020)

	Ref	Expression
Assertion	inxpxrn	⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) ) = ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		xrnrel	⊢ Rel ( ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) )
2		relinxp	⊢ Rel ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) )
3		brxrn2	⊢ ( 𝑢 ∈ V → ( 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) )
4	3	elv	⊢ ( 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) )
5	4	anbi2i	⊢ ( ( 𝑢 ∈ 𝐴 ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ) ↔ ( 𝑢 ∈ 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) )
6	5	anbi2i	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ) ) ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
7		xrninxp2	⊢ ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) = { ⟨ 𝑢 , 𝑥 ⟩ ∣ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ) ) }
8	7	brabidgaw	⊢ ( 𝑢 ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) 𝑥 ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ 𝑢 ( 𝑅 ⋉ 𝑆 ) 𝑥 ) ) )
9		brxrn2	⊢ ( 𝑢 ∈ V → ( 𝑢 ( ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) ) 𝑥 ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ) )
10	9	elv	⊢ ( 𝑢 ( ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) ) 𝑥 ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) )
11		3anass	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ) )
12	11	2exbii	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ) )
13		brinxp2	⊢ ( 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 𝑅 𝑦 ) )
14		brinxp2	⊢ ( 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ↔ ( ( 𝑢 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑢 𝑆 𝑧 ) )
15	13 14	anbi12i	⊢ ( ( 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ↔ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 𝑅 𝑦 ) ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑢 𝑆 𝑧 ) ) )
16		anan	⊢ ( ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑢 𝑅 𝑦 ) ∧ ( ( 𝑢 ∈ 𝐴 ∧ 𝑧 ∈ 𝐶 ) ∧ 𝑢 𝑆 𝑧 ) ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
17	15 16	bitri	⊢ ( ( 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ↔ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
18	17	anbi2i	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ) )
19		anass	⊢ ( ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ) )
20		eqelb	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑥 ∈ ( 𝐵 × 𝐶 ) ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐵 × 𝐶 ) ) )
21		opelxp	⊢ ( ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐵 × 𝐶 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) )
22	21	anbi2i	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝐵 × 𝐶 ) ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) )
23	20 22	bitr2i	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑥 ∈ ( 𝐵 × 𝐶 ) ) )
24	23	anbi1i	⊢ ( ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐶 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ↔ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑥 ∈ ( 𝐵 × 𝐶 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
25	18 19 24	3bitr2i	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ) ↔ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑥 ∈ ( 𝐵 × 𝐶 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
26		ancom	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑥 ∈ ( 𝐵 × 𝐶 ) ) ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) )
27	26	anbi1i	⊢ ( ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑥 ∈ ( 𝐵 × 𝐶 ) ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ↔ ( ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
28		anass	⊢ ( ( ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ) )
29	25 27 28	3bitri	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ) ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ) )
30		an12	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ↔ ( 𝑢 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
31		3anass	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ↔ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) )
32	31	anbi2i	⊢ ( ( 𝑢 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ↔ ( 𝑢 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
33	30 32	bitr4i	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ↔ ( 𝑢 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) )
34	33	anbi2i	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ) ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
35	29 34	bitri	⊢ ( ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ) ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
36	35	2exbii	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ) ↔ ∃ 𝑦 ∃ 𝑧 ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
37		19.42vv	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑢 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
38		19.42vv	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑢 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ↔ ( 𝑢 ∈ 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) )
39	38	anbi2i	⊢ ( ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑢 ∈ 𝐴 ∧ ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
40	36 37 39	3bitri	⊢ ( ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ ( 𝑢 ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) 𝑦 ∧ 𝑢 ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) 𝑧 ) ) ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
41	10 12 40	3bitri	⊢ ( 𝑢 ( ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) ) 𝑥 ↔ ( 𝑥 ∈ ( 𝐵 × 𝐶 ) ∧ ( 𝑢 ∈ 𝐴 ∧ ∃ 𝑦 ∃ 𝑧 ( 𝑥 = ⟨ 𝑦 , 𝑧 ⟩ ∧ 𝑢 𝑅 𝑦 ∧ 𝑢 𝑆 𝑧 ) ) ) )
42	6 8 41	3bitr4ri	⊢ ( 𝑢 ( ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) ) 𝑥 ↔ 𝑢 ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) ) 𝑥 )
43	1 2 42	eqbrriv	⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) ) = ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) )