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 𝑥 ∈ 𝐼 𝐴 = ( X 𝑥 ∈ 𝐼 𝐵 ∩ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simprl ⊢ ( ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 ∧ ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) ) → 𝑧 Fn 𝐼 )
2 ssel ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 → ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) )
3 2 ral2imi ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 → ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) )
4 3 adantr ⊢ ( ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 ∧ 𝑧 Fn 𝐼 ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 → ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) )
5 4 impr ⊢ ( ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 ∧ ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 )
6 eleq2 ⊢ ( 𝐴 = if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) → ( ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ↔ ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
7 eleq2 ⊢ ( 𝐵 = if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) → ( ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ↔ ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
8 simplr ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) ∧ 𝑥 = 𝑦 ) → ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 )
9 ssel2 ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) → ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 )
10 9 adantr ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) ∧ ¬ 𝑥 = 𝑦 ) → ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 )
11 6 7 8 10 ifbothda ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) → ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) )
12 11 ex ⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 → ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
13 12 ral2imi ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 → ( ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 → ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
14 13 adantr ⊢ ( ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 ∧ 𝑧 Fn 𝐼 ) → ( ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 → ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
15 14 impr ⊢ ( ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 ∧ ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) )
16 1 15 jca ⊢ ( ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 ∧ ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) ) → ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
17 16 ralrimivw ⊢ ( ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 ∧ ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) ) → ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
18 1 5 17 jca31 ⊢ ( ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 ∧ ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) ) → ( ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) ) )
19 simprll ⊢ ( ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 ∧ ( ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) ) ) → 𝑧 Fn 𝐼 )
20 simpr ⊢ ( ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) )
21 20 ralimi ⊢ ( ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) → ∀ 𝑦 ∈ 𝐼 ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) )
22 ralcom ⊢ ( ∀ 𝑦 ∈ 𝐼 ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) )
23 iftrue ⊢ ( 𝑥 = 𝑦 → if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) = 𝐴 )
24 23 equcoms ⊢ ( 𝑦 = 𝑥 → if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) = 𝐴 )
25 24 eleq2d ⊢ ( 𝑦 = 𝑥 → ( ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ↔ ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) )
26 25 rspcva ⊢ ( ( 𝑥 ∈ 𝐼 ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) → ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 )
27 26 ralimiaa ⊢ ( ∀ 𝑥 ∈ 𝐼 ∀ 𝑦 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) → ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 )
28 22 27 sylbi ⊢ ( ∀ 𝑦 ∈ 𝐼 ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) → ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 )
29 21 28 syl ⊢ ( ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 )
30 29 ad2antll ⊢ ( ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 ∧ ( ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) ) ) → ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 )
31 19 30 jca ⊢ ( ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 ∧ ( ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) ) ) → ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) )
32 18 31 impbida ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 → ( ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) ↔ ( ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) ) ) )
33 vex ⊢ 𝑧 ∈ V
34 33 elixp ⊢ ( 𝑧 ∈ X 𝑥 ∈ 𝐼 𝐴 ↔ ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐴 ) )
35 elin ⊢ ( 𝑧 ∈ ( X 𝑥 ∈ 𝐼 𝐵 ∩ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) ↔ ( 𝑧 ∈ X 𝑥 ∈ 𝐼 𝐵 ∧ 𝑧 ∈ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
36 33 elixp ⊢ ( 𝑧 ∈ X 𝑥 ∈ 𝐼 𝐵 ↔ ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) )
37 eliin ⊢ ( 𝑧 ∈ V → ( 𝑧 ∈ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐼 𝑧 ∈ X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
38 37 elv ⊢ ( 𝑧 ∈ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐼 𝑧 ∈ X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) )
39 33 elixp ⊢ ( 𝑧 ∈ X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ↔ ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
40 39 ralbii ⊢ ( ∀ 𝑦 ∈ 𝐼 𝑧 ∈ X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
41 38 40 bitri ⊢ ( 𝑧 ∈ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ↔ ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )
42 36 41 anbi12i ⊢ ( ( 𝑧 ∈ X 𝑥 ∈ 𝐼 𝐵 ∧ 𝑧 ∈ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) ↔ ( ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) ) )
43 35 42 bitri ⊢ ( 𝑧 ∈ ( X 𝑥 ∈ 𝐼 𝐵 ∩ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) ↔ ( ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ 𝐵 ) ∧ ∀ 𝑦 ∈ 𝐼 ( 𝑧 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑧 ‘ 𝑥 ) ∈ if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) ) )
44 32 34 43 3bitr4g ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 → ( 𝑧 ∈ X 𝑥 ∈ 𝐼 𝐴 ↔ 𝑧 ∈ ( X 𝑥 ∈ 𝐼 𝐵 ∩ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) ) )
45 44 eqrdv ⊢ ( ∀ 𝑥 ∈ 𝐼 𝐴 ⊆ 𝐵 → X 𝑥 ∈ 𝐼 𝐴 = ( X 𝑥 ∈ 𝐼 𝐵 ∩ ∩ 𝑦 ∈ 𝐼 X 𝑥 ∈ 𝐼 if ( 𝑥 = 𝑦 , 𝐴 , 𝐵 ) ) )