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 ${⊢}\left({R}\cap \left({A}×{B}\right)\right)⋉\left({S}\cap \left({A}×{C}\right)\right)={R}⋉{S}\cap \left({A}×\left({B}×{C}\right)\right)$

Proof

Step Hyp Ref Expression
1 xrnrel ${⊢}\mathrm{Rel}\left({R}\cap \left({A}×{B}\right)\right)⋉\left({S}\cap \left({A}×{C}\right)\right)$
2 relinxp ${⊢}\mathrm{Rel}\left({R}⋉{S}\cap \left({A}×\left({B}×{C}\right)\right)\right)$
3 brxrn2 ${⊢}{u}\in \mathrm{V}\to \left({u}{R}⋉{S}{x}↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)$
4 3 elv ${⊢}{u}{R}⋉{S}{x}↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)$
5 4 anbi2i ${⊢}\left({u}\in {A}\wedge {u}{R}⋉{S}{x}\right)↔\left({u}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)$
6 5 anbi2i ${⊢}\left({x}\in \left({B}×{C}\right)\wedge \left({u}\in {A}\wedge {u}{R}⋉{S}{x}\right)\right)↔\left({x}\in \left({B}×{C}\right)\wedge \left({u}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
7 xrninxp2 ${⊢}{R}⋉{S}\cap \left({A}×\left({B}×{C}\right)\right)=\left\{⟨{u},{x}⟩|\left({x}\in \left({B}×{C}\right)\wedge \left({u}\in {A}\wedge {u}{R}⋉{S}{x}\right)\right)\right\}$
8 7 brabidgaw ${⊢}{u}\left({R}⋉{S}\cap \left({A}×\left({B}×{C}\right)\right)\right){x}↔\left({x}\in \left({B}×{C}\right)\wedge \left({u}\in {A}\wedge {u}{R}⋉{S}{x}\right)\right)$
9 brxrn2 ${⊢}{u}\in \mathrm{V}\to \left({u}\left({R}\cap \left({A}×{B}\right)\right)⋉\left({S}\cap \left({A}×{C}\right)\right){x}↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge {u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)\right)$
10 9 elv ${⊢}{u}\left({R}\cap \left({A}×{B}\right)\right)⋉\left({S}\cap \left({A}×{C}\right)\right){x}↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge {u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)$
11 3anass ${⊢}\left({x}=⟨{y},{z}⟩\wedge {u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)↔\left({x}=⟨{y},{z}⟩\wedge \left({u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)\right)$
12 11 2exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge {u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge \left({u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)\right)$
13 brinxp2 ${⊢}{u}\left({R}\cap \left({A}×{B}\right)\right){y}↔\left(\left({u}\in {A}\wedge {y}\in {B}\right)\wedge {u}{R}{y}\right)$
14 brinxp2 ${⊢}{u}\left({S}\cap \left({A}×{C}\right)\right){z}↔\left(\left({u}\in {A}\wedge {z}\in {C}\right)\wedge {u}{S}{z}\right)$
15 13 14 anbi12i ${⊢}\left({u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)↔\left(\left(\left({u}\in {A}\wedge {y}\in {B}\right)\wedge {u}{R}{y}\right)\wedge \left(\left({u}\in {A}\wedge {z}\in {C}\right)\wedge {u}{S}{z}\right)\right)$
16 anan ${⊢}\left(\left(\left({u}\in {A}\wedge {y}\in {B}\right)\wedge {u}{R}{y}\right)\wedge \left(\left({u}\in {A}\wedge {z}\in {C}\right)\wedge {u}{S}{z}\right)\right)↔\left(\left({y}\in {B}\wedge {z}\in {C}\right)\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
17 15 16 bitri ${⊢}\left({u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)↔\left(\left({y}\in {B}\wedge {z}\in {C}\right)\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
18 17 anbi2i ${⊢}\left({x}=⟨{y},{z}⟩\wedge \left({u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)\right)↔\left({x}=⟨{y},{z}⟩\wedge \left(\left({y}\in {B}\wedge {z}\in {C}\right)\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)\right)$
19 anass ${⊢}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {B}\wedge {z}\in {C}\right)\right)\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)↔\left({x}=⟨{y},{z}⟩\wedge \left(\left({y}\in {B}\wedge {z}\in {C}\right)\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)\right)$
20 eqelb ${⊢}\left({x}=⟨{y},{z}⟩\wedge {x}\in \left({B}×{C}\right)\right)↔\left({x}=⟨{y},{z}⟩\wedge ⟨{y},{z}⟩\in \left({B}×{C}\right)\right)$
21 opelxp ${⊢}⟨{y},{z}⟩\in \left({B}×{C}\right)↔\left({y}\in {B}\wedge {z}\in {C}\right)$
22 21 anbi2i ${⊢}\left({x}=⟨{y},{z}⟩\wedge ⟨{y},{z}⟩\in \left({B}×{C}\right)\right)↔\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {B}\wedge {z}\in {C}\right)\right)$
23 20 22 bitr2i ${⊢}\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {B}\wedge {z}\in {C}\right)\right)↔\left({x}=⟨{y},{z}⟩\wedge {x}\in \left({B}×{C}\right)\right)$
24 23 anbi1i ${⊢}\left(\left({x}=⟨{y},{z}⟩\wedge \left({y}\in {B}\wedge {z}\in {C}\right)\right)\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)↔\left(\left({x}=⟨{y},{z}⟩\wedge {x}\in \left({B}×{C}\right)\right)\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
25 18 19 24 3bitr2i ${⊢}\left({x}=⟨{y},{z}⟩\wedge \left({u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)\right)↔\left(\left({x}=⟨{y},{z}⟩\wedge {x}\in \left({B}×{C}\right)\right)\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
26 ancom ${⊢}\left({x}=⟨{y},{z}⟩\wedge {x}\in \left({B}×{C}\right)\right)↔\left({x}\in \left({B}×{C}\right)\wedge {x}=⟨{y},{z}⟩\right)$
27 26 anbi1i ${⊢}\left(\left({x}=⟨{y},{z}⟩\wedge {x}\in \left({B}×{C}\right)\right)\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)↔\left(\left({x}\in \left({B}×{C}\right)\wedge {x}=⟨{y},{z}⟩\right)\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
28 anass ${⊢}\left(\left({x}\in \left({B}×{C}\right)\wedge {x}=⟨{y},{z}⟩\right)\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)↔\left({x}\in \left({B}×{C}\right)\wedge \left({x}=⟨{y},{z}⟩\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)\right)$
29 25 27 28 3bitri ${⊢}\left({x}=⟨{y},{z}⟩\wedge \left({u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)\right)↔\left({x}\in \left({B}×{C}\right)\wedge \left({x}=⟨{y},{z}⟩\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)\right)$
30 an12 ${⊢}\left({x}=⟨{y},{z}⟩\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)↔\left({u}\in {A}\wedge \left({x}=⟨{y},{z}⟩\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
31 3anass ${⊢}\left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)↔\left({x}=⟨{y},{z}⟩\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)$
32 31 anbi2i ${⊢}\left({u}\in {A}\wedge \left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)↔\left({u}\in {A}\wedge \left({x}=⟨{y},{z}⟩\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
33 30 32 bitr4i ${⊢}\left({x}=⟨{y},{z}⟩\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)↔\left({u}\in {A}\wedge \left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)$
34 33 anbi2i ${⊢}\left({x}\in \left({B}×{C}\right)\wedge \left({x}=⟨{y},{z}⟩\wedge \left({u}\in {A}\wedge \left({u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)\right)↔\left({x}\in \left({B}×{C}\right)\wedge \left({u}\in {A}\wedge \left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
35 29 34 bitri ${⊢}\left({x}=⟨{y},{z}⟩\wedge \left({u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)\right)↔\left({x}\in \left({B}×{C}\right)\wedge \left({u}\in {A}\wedge \left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
36 35 2exbii ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge \left({u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)\right)↔\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({B}×{C}\right)\wedge \left({u}\in {A}\wedge \left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
37 19.42vv ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({B}×{C}\right)\wedge \left({u}\in {A}\wedge \left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)↔\left({x}\in \left({B}×{C}\right)\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({u}\in {A}\wedge \left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
38 19.42vv ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({u}\in {A}\wedge \left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)↔\left({u}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)$
39 38 anbi2i ${⊢}\left({x}\in \left({B}×{C}\right)\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({u}\in {A}\wedge \left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)↔\left({x}\in \left({B}×{C}\right)\wedge \left({u}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
40 36 37 39 3bitri ${⊢}\exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge \left({u}\left({R}\cap \left({A}×{B}\right)\right){y}\wedge {u}\left({S}\cap \left({A}×{C}\right)\right){z}\right)\right)↔\left({x}\in \left({B}×{C}\right)\wedge \left({u}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
41 10 12 40 3bitri ${⊢}{u}\left({R}\cap \left({A}×{B}\right)\right)⋉\left({S}\cap \left({A}×{C}\right)\right){x}↔\left({x}\in \left({B}×{C}\right)\wedge \left({u}\in {A}\wedge \exists {y}\phantom{\rule{.4em}{0ex}}\exists {z}\phantom{\rule{.4em}{0ex}}\left({x}=⟨{y},{z}⟩\wedge {u}{R}{y}\wedge {u}{S}{z}\right)\right)\right)$
42 6 8 41 3bitr4ri ${⊢}{u}\left({R}\cap \left({A}×{B}\right)\right)⋉\left({S}\cap \left({A}×{C}\right)\right){x}↔{u}\left({R}⋉{S}\cap \left({A}×\left({B}×{C}\right)\right)\right){x}$
43 1 2 42 eqbrriv ${⊢}\left({R}\cap \left({A}×{B}\right)\right)⋉\left({S}\cap \left({A}×{C}\right)\right)={R}⋉{S}\cap \left({A}×\left({B}×{C}\right)\right)$