This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝑅 ∩ ( 𝐴 × 𝐵 ) ) ⋉ ( 𝑆 ∩ ( 𝐴 × 𝐶 ) ) ) = ( ( 𝑅 ⋉ 𝑆 ) ∩ ( 𝐴 × ( 𝐵 × 𝐶 ) ) )