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 ∈ I A ⊆ B → ⨉ x ∈ I A = ⨉ x ∈ I B ∩ ⋂ y ∈ I ⨉ x ∈ I if x = y A B

Proof

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