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 
|- ( A. x e. I A C_ B -> X_ x e. I A = ( X_ x e. I B i^i |^|_ y e. I X_ x e. I if ( x = y , A , B ) ) )

Proof

Step Hyp Ref Expression
1 simprl 
 |-  ( ( A. x e. I A C_ B /\ ( z Fn I /\ A. x e. I ( z ` x ) e. A ) ) -> z Fn I )
2 ssel 
 |-  ( A C_ B -> ( ( z ` x ) e. A -> ( z ` x ) e. B ) )
3 2 ral2imi 
 |-  ( A. x e. I A C_ B -> ( A. x e. I ( z ` x ) e. A -> A. x e. I ( z ` x ) e. B ) )
4 3 adantr 
 |-  ( ( A. x e. I A C_ B /\ z Fn I ) -> ( A. x e. I ( z ` x ) e. A -> A. x e. I ( z ` x ) e. B ) )
5 4 impr 
 |-  ( ( A. x e. I A C_ B /\ ( z Fn I /\ A. x e. I ( z ` x ) e. A ) ) -> A. x e. I ( z ` x ) e. B )
6 eleq2 
 |-  ( A = if ( x = y , A , B ) -> ( ( z ` x ) e. A <-> ( z ` x ) e. if ( x = y , A , B ) ) )
7 eleq2 
 |-  ( B = if ( x = y , A , B ) -> ( ( z ` x ) e. B <-> ( z ` x ) e. if ( x = y , A , B ) ) )
8 simplr 
 |-  ( ( ( A C_ B /\ ( z ` x ) e. A ) /\ x = y ) -> ( z ` x ) e. A )
9 ssel2 
 |-  ( ( A C_ B /\ ( z ` x ) e. A ) -> ( z ` x ) e. B )
10 9 adantr 
 |-  ( ( ( A C_ B /\ ( z ` x ) e. A ) /\ -. x = y ) -> ( z ` x ) e. B )
11 6 7 8 10 ifbothda 
 |-  ( ( A C_ B /\ ( z ` x ) e. A ) -> ( z ` x ) e. if ( x = y , A , B ) )
12 11 ex 
 |-  ( A C_ B -> ( ( z ` x ) e. A -> ( z ` x ) e. if ( x = y , A , B ) ) )
13 12 ral2imi 
 |-  ( A. x e. I A C_ B -> ( A. x e. I ( z ` x ) e. A -> A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) )
14 13 adantr 
 |-  ( ( A. x e. I A C_ B /\ z Fn I ) -> ( A. x e. I ( z ` x ) e. A -> A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) )
15 14 impr 
 |-  ( ( A. x e. I A C_ B /\ ( z Fn I /\ A. x e. I ( z ` x ) e. A ) ) -> A. x e. I ( z ` x ) e. if ( x = y , A , B ) )
16 1 15 jca 
 |-  ( ( A. x e. I A C_ B /\ ( z Fn I /\ A. x e. I ( z ` x ) e. A ) ) -> ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) )
17 16 ralrimivw 
 |-  ( ( A. x e. I A C_ B /\ ( z Fn I /\ A. x e. I ( z ` x ) e. A ) ) -> A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) )
18 1 5 17 jca31 
 |-  ( ( A. x e. I A C_ B /\ ( z Fn I /\ A. x e. I ( z ` x ) e. A ) ) -> ( ( z Fn I /\ A. x e. I ( z ` x ) e. B ) /\ A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) ) )
19 simprll 
 |-  ( ( A. x e. I A C_ B /\ ( ( z Fn I /\ A. x e. I ( z ` x ) e. B ) /\ A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) ) ) -> z Fn I )
20 simpr 
 |-  ( ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) -> A. x e. I ( z ` x ) e. if ( x = y , A , B ) )
21 20 ralimi 
 |-  ( A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) -> A. y e. I A. x e. I ( z ` x ) e. if ( x = y , A , B ) )
22 ralcom 
 |-  ( A. y e. I A. x e. I ( z ` x ) e. if ( x = y , A , B ) <-> A. x e. I A. y e. I ( z ` x ) e. 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 ) e. if ( x = y , A , B ) <-> ( z ` x ) e. A ) )
26 25 rspcva 
 |-  ( ( x e. I /\ A. y e. I ( z ` x ) e. if ( x = y , A , B ) ) -> ( z ` x ) e. A )
27 26 ralimiaa 
 |-  ( A. x e. I A. y e. I ( z ` x ) e. if ( x = y , A , B ) -> A. x e. I ( z ` x ) e. A )
28 22 27 sylbi 
 |-  ( A. y e. I A. x e. I ( z ` x ) e. if ( x = y , A , B ) -> A. x e. I ( z ` x ) e. A )
29 21 28 syl 
 |-  ( A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) -> A. x e. I ( z ` x ) e. A )
30 29 ad2antll 
 |-  ( ( A. x e. I A C_ B /\ ( ( z Fn I /\ A. x e. I ( z ` x ) e. B ) /\ A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) ) ) -> A. x e. I ( z ` x ) e. A )
31 19 30 jca 
 |-  ( ( A. x e. I A C_ B /\ ( ( z Fn I /\ A. x e. I ( z ` x ) e. B ) /\ A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) ) ) -> ( z Fn I /\ A. x e. I ( z ` x ) e. A ) )
32 18 31 impbida 
 |-  ( A. x e. I A C_ B -> ( ( z Fn I /\ A. x e. I ( z ` x ) e. A ) <-> ( ( z Fn I /\ A. x e. I ( z ` x ) e. B ) /\ A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) ) ) )
33 vex 
 |-  z e. _V
34 33 elixp 
 |-  ( z e. X_ x e. I A <-> ( z Fn I /\ A. x e. I ( z ` x ) e. A ) )
35 elin 
 |-  ( z e. ( X_ x e. I B i^i |^|_ y e. I X_ x e. I if ( x = y , A , B ) ) <-> ( z e. X_ x e. I B /\ z e. |^|_ y e. I X_ x e. I if ( x = y , A , B ) ) )
36 33 elixp 
 |-  ( z e. X_ x e. I B <-> ( z Fn I /\ A. x e. I ( z ` x ) e. B ) )
37 eliin 
 |-  ( z e. _V -> ( z e. |^|_ y e. I X_ x e. I if ( x = y , A , B ) <-> A. y e. I z e. X_ x e. I if ( x = y , A , B ) ) )
38 37 elv 
 |-  ( z e. |^|_ y e. I X_ x e. I if ( x = y , A , B ) <-> A. y e. I z e. X_ x e. I if ( x = y , A , B ) )
39 33 elixp 
 |-  ( z e. X_ x e. I if ( x = y , A , B ) <-> ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) )
40 39 ralbii 
 |-  ( A. y e. I z e. X_ x e. I if ( x = y , A , B ) <-> A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) )
41 38 40 bitri 
 |-  ( z e. |^|_ y e. I X_ x e. I if ( x = y , A , B ) <-> A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) )
42 36 41 anbi12i 
 |-  ( ( z e. X_ x e. I B /\ z e. |^|_ y e. I X_ x e. I if ( x = y , A , B ) ) <-> ( ( z Fn I /\ A. x e. I ( z ` x ) e. B ) /\ A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) ) )
43 35 42 bitri 
 |-  ( z e. ( X_ x e. I B i^i |^|_ y e. I X_ x e. I if ( x = y , A , B ) ) <-> ( ( z Fn I /\ A. x e. I ( z ` x ) e. B ) /\ A. y e. I ( z Fn I /\ A. x e. I ( z ` x ) e. if ( x = y , A , B ) ) ) )
44 32 34 43 3bitr4g 
 |-  ( A. x e. I A C_ B -> ( z e. X_ x e. I A <-> z e. ( X_ x e. I B i^i |^|_ y e. I X_ x e. I if ( x = y , A , B ) ) ) )
45 44 eqrdv 
 |-  ( A. x e. I A C_ B -> X_ x e. I A = ( X_ x e. I B i^i |^|_ y e. I X_ x e. I if ( x = y , A , B ) ) )