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 ⊢∀x∈IA⊆B→⨉x∈IA=⨉x∈IB∩⋂y∈I⨉x∈Iifx=yAB

Proof

Step Hyp Ref Expression
1 simprl ⊢∀x∈IA⊆B∧zFnI∧∀x∈Iz⁡x∈A→zFnI
2 ssel ⊢A⊆B→z⁡x∈A→z⁡x∈B
3 2 ral2imi ⊢∀x∈IA⊆B→∀x∈Iz⁡x∈A→∀x∈Iz⁡x∈B
4 3 adantr ⊢∀x∈IA⊆B∧zFnI→∀x∈Iz⁡x∈A→∀x∈Iz⁡x∈B
5 4 impr ⊢∀x∈IA⊆B∧zFnI∧∀x∈Iz⁡x∈A→∀x∈Iz⁡x∈B
6 eleq2 ⊢A=ifx=yAB→z⁡x∈A↔z⁡x∈ifx=yAB
7 eleq2 ⊢B=ifx=yAB→z⁡x∈B↔z⁡x∈ifx=yAB
8 simplr ⊢A⊆B∧z⁡x∈A∧x=y→z⁡x∈A
9 ssel2 ⊢A⊆B∧z⁡x∈A→z⁡x∈B
10 9 adantr ⊢A⊆B∧z⁡x∈A∧¬x=y→z⁡x∈B
11 6 7 8 10 ifbothda ⊢A⊆B∧z⁡x∈A→z⁡x∈ifx=yAB
12 11 ex ⊢A⊆B→z⁡x∈A→z⁡x∈ifx=yAB
13 12 ral2imi ⊢∀x∈IA⊆B→∀x∈Iz⁡x∈A→∀x∈Iz⁡x∈ifx=yAB
14 13 adantr ⊢∀x∈IA⊆B∧zFnI→∀x∈Iz⁡x∈A→∀x∈Iz⁡x∈ifx=yAB
15 14 impr ⊢∀x∈IA⊆B∧zFnI∧∀x∈Iz⁡x∈A→∀x∈Iz⁡x∈ifx=yAB
16 1 15 jca ⊢∀x∈IA⊆B∧zFnI∧∀x∈Iz⁡x∈A→zFnI∧∀x∈Iz⁡x∈ifx=yAB
17 16 ralrimivw ⊢∀x∈IA⊆B∧zFnI∧∀x∈Iz⁡x∈A→∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB
18 1 5 17 jca31 ⊢∀x∈IA⊆B∧zFnI∧∀x∈Iz⁡x∈A→zFnI∧∀x∈Iz⁡x∈B∧∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB
19 simprll ⊢∀x∈IA⊆B∧zFnI∧∀x∈Iz⁡x∈B∧∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB→zFnI
20 simpr ⊢zFnI∧∀x∈Iz⁡x∈ifx=yAB→∀x∈Iz⁡x∈ifx=yAB
21 20 ralimi ⊢∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB→∀y∈I∀x∈Iz⁡x∈ifx=yAB
22 ralcom ⊢∀y∈I∀x∈Iz⁡x∈ifx=yAB↔∀x∈I∀y∈Iz⁡x∈ifx=yAB
23 iftrue ⊢x=y→ifx=yAB=A
24 23 equcoms ⊢y=x→ifx=yAB=A
25 24 eleq2d ⊢y=x→z⁡x∈ifx=yAB↔z⁡x∈A
26 25 rspcva ⊢x∈I∧∀y∈Iz⁡x∈ifx=yAB→z⁡x∈A
27 26 ralimiaa ⊢∀x∈I∀y∈Iz⁡x∈ifx=yAB→∀x∈Iz⁡x∈A
28 22 27 sylbi ⊢∀y∈I∀x∈Iz⁡x∈ifx=yAB→∀x∈Iz⁡x∈A
29 21 28 syl ⊢∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB→∀x∈Iz⁡x∈A
30 29 ad2antll ⊢∀x∈IA⊆B∧zFnI∧∀x∈Iz⁡x∈B∧∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB→∀x∈Iz⁡x∈A
31 19 30 jca ⊢∀x∈IA⊆B∧zFnI∧∀x∈Iz⁡x∈B∧∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB→zFnI∧∀x∈Iz⁡x∈A
32 18 31 impbida ⊢∀x∈IA⊆B→zFnI∧∀x∈Iz⁡x∈A↔zFnI∧∀x∈Iz⁡x∈B∧∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB
33 vex ⊢z∈V
34 33 elixp ⊢z∈⨉x∈IA↔zFnI∧∀x∈Iz⁡x∈A
35 elin ⊢z∈⨉x∈IB∩⋂y∈I⨉x∈Iifx=yAB↔z∈⨉x∈IB∧z∈⋂y∈I⨉x∈Iifx=yAB
36 33 elixp ⊢z∈⨉x∈IB↔zFnI∧∀x∈Iz⁡x∈B
37 eliin ⊢z∈V→z∈⋂y∈I⨉x∈Iifx=yAB↔∀y∈Iz∈⨉x∈Iifx=yAB
38 37 elv ⊢z∈⋂y∈I⨉x∈Iifx=yAB↔∀y∈Iz∈⨉x∈Iifx=yAB
39 33 elixp ⊢z∈⨉x∈Iifx=yAB↔zFnI∧∀x∈Iz⁡x∈ifx=yAB
40 39 ralbii ⊢∀y∈Iz∈⨉x∈Iifx=yAB↔∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB
41 38 40 bitri ⊢z∈⋂y∈I⨉x∈Iifx=yAB↔∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB
42 36 41 anbi12i ⊢z∈⨉x∈IB∧z∈⋂y∈I⨉x∈Iifx=yAB↔zFnI∧∀x∈Iz⁡x∈B∧∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB
43 35 42 bitri ⊢z∈⨉x∈IB∩⋂y∈I⨉x∈Iifx=yAB↔zFnI∧∀x∈Iz⁡x∈B∧∀y∈IzFnI∧∀x∈Iz⁡x∈ifx=yAB
44 32 34 43 3bitr4g ⊢∀x∈IA⊆B→z∈⨉x∈IA↔z∈⨉x∈IB∩⋂y∈I⨉x∈Iifx=yAB
45 44 eqrdv ⊢∀x∈IA⊆B→⨉x∈IA=⨉x∈IB∩⋂y∈I⨉x∈Iifx=yAB