# Metamath Proof Explorer

## Theorem boxriin

Description: A rectangular subset of a rectangular set can be recovered as the relative intersection of single-axis restrictions. (Contributed by Stefan O'Rear, 22-Feb-2015)

Ref Expression
Assertion boxriin ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\to \underset{{x}\in {I}}{⨉}{A}=\underset{{x}\in {I}}{⨉}{B}\cap \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)$

### Proof

Step Hyp Ref Expression
1 simprl ${⊢}\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\wedge \left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\right)\right)\to {z}Fn{I}$
2 ssel ${⊢}{A}\subseteq {B}\to \left({z}\left({x}\right)\in {A}\to {z}\left({x}\right)\in {B}\right)$
3 2 ral2imi ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)$
4 3 adantr ${⊢}\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\wedge {z}Fn{I}\right)\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)$
5 4 impr ${⊢}\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\wedge \left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}$
6 eleq2 ${⊢}{A}=if\left({x}={y},{A},{B}\right)\to \left({z}\left({x}\right)\in {A}↔{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)$
7 eleq2 ${⊢}{B}=if\left({x}={y},{A},{B}\right)\to \left({z}\left({x}\right)\in {B}↔{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)$
8 simplr ${⊢}\left(\left({A}\subseteq {B}\wedge {z}\left({x}\right)\in {A}\right)\wedge {x}={y}\right)\to {z}\left({x}\right)\in {A}$
9 ssel2 ${⊢}\left({A}\subseteq {B}\wedge {z}\left({x}\right)\in {A}\right)\to {z}\left({x}\right)\in {B}$
10 9 adantr ${⊢}\left(\left({A}\subseteq {B}\wedge {z}\left({x}\right)\in {A}\right)\wedge ¬{x}={y}\right)\to {z}\left({x}\right)\in {B}$
11 6 7 8 10 ifbothda ${⊢}\left({A}\subseteq {B}\wedge {z}\left({x}\right)\in {A}\right)\to {z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)$
12 11 ex ${⊢}{A}\subseteq {B}\to \left({z}\left({x}\right)\in {A}\to {z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)$
13 12 ral2imi ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)$
14 13 adantr ${⊢}\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\wedge {z}Fn{I}\right)\to \left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)$
15 14 impr ${⊢}\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\wedge \left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)$
16 1 15 jca ${⊢}\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\wedge \left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\right)\right)\to \left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)$
17 16 ralrimivw ${⊢}\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\wedge \left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\right)\right)\to \forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)$
18 1 5 17 jca31 ${⊢}\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\wedge \left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\right)\right)\to \left(\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)\wedge \forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)\right)$
19 simprll ${⊢}\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\wedge \left(\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)\wedge \forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)\right)\right)\to {z}Fn{I}$
20 simpr ${⊢}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)$
21 20 ralimi ${⊢}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)\to \forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)$
22 ralcom ${⊢}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)↔\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)$
23 iftrue ${⊢}{x}={y}\to if\left({x}={y},{A},{B}\right)={A}$
24 23 equcoms ${⊢}{y}={x}\to if\left({x}={y},{A},{B}\right)={A}$
25 24 eleq2d ${⊢}{y}={x}\to \left({z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)↔{z}\left({x}\right)\in {A}\right)$
26 25 rspcva ${⊢}\left({x}\in {I}\wedge \forall {y}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)\to {z}\left({x}\right)\in {A}$
27 26 ralimiaa ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}$
28 22 27 sylbi ${⊢}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}$
29 21 28 syl ${⊢}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}$
30 29 ad2antll ${⊢}\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\wedge \left(\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)\wedge \forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)\right)\right)\to \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}$
31 19 30 jca ${⊢}\left(\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\wedge \left(\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)\wedge \forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)\right)\right)\to \left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\right)$
32 18 31 impbida ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\to \left(\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\right)↔\left(\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)\wedge \forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)\right)\right)$
33 vex ${⊢}{z}\in \mathrm{V}$
34 33 elixp ${⊢}{z}\in \underset{{x}\in {I}}{⨉}{A}↔\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {A}\right)$
35 elin ${⊢}{z}\in \left(\underset{{x}\in {I}}{⨉}{B}\cap \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)\right)↔\left({z}\in \underset{{x}\in {I}}{⨉}{B}\wedge {z}\in \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)\right)$
36 33 elixp ${⊢}{z}\in \underset{{x}\in {I}}{⨉}{B}↔\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)$
37 eliin ${⊢}{z}\in \mathrm{V}\to \left({z}\in \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)↔\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}{z}\in \underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)\right)$
38 37 elv ${⊢}{z}\in \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)↔\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}{z}\in \underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)$
39 33 elixp ${⊢}{z}\in \underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)↔\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)$
40 39 ralbii ${⊢}\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}{z}\in \underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)↔\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)$
41 38 40 bitri ${⊢}{z}\in \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)↔\forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)$
42 36 41 anbi12i ${⊢}\left({z}\in \underset{{x}\in {I}}{⨉}{B}\wedge {z}\in \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)\right)↔\left(\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)\wedge \forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)\right)$
43 35 42 bitri ${⊢}{z}\in \left(\underset{{x}\in {I}}{⨉}{B}\cap \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)\right)↔\left(\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in {B}\right)\wedge \forall {y}\in {I}\phantom{\rule{.4em}{0ex}}\left({z}Fn{I}\wedge \forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{z}\left({x}\right)\in if\left({x}={y},{A},{B}\right)\right)\right)$
44 32 34 43 3bitr4g ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\to \left({z}\in \underset{{x}\in {I}}{⨉}{A}↔{z}\in \left(\underset{{x}\in {I}}{⨉}{B}\cap \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)\right)\right)$
45 44 eqrdv ${⊢}\forall {x}\in {I}\phantom{\rule{.4em}{0ex}}{A}\subseteq {B}\to \underset{{x}\in {I}}{⨉}{A}=\underset{{x}\in {I}}{⨉}{B}\cap \bigcap _{{y}\in {I}}\underset{{x}\in {I}}{⨉}if\left({x}={y},{A},{B}\right)$