Theorem boxriin 7950

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.)

Assertion

Ref	Expression
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 ) ) )

Distinct variable groups:   y, A   y, B   x, I, y

Allowed substitution hints:   A( x)   B( x)

Proof of Theorem boxriin

Dummy variable z is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simprl 794	. . . . 5 |- ( ( A. x e. I A C_ B /\ ( z Fn I /\ A. x e. I ( z ` x ) e. A ) ) -> z Fn I )
2		ssel 3597	. . . . . . . 8 |- ( A C_ B -> ( ( z ` x ) e. A -> ( z ` x ) e. B ) )
3	2	ral2imi 2947	. . . . . . 7 |- ( 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 481	. . . . . 6 |- ( ( 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 649	. . . . 5 |- ( ( 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 2690	. . . . . . . . . . . 12 |- ( A = if ( x = y , A , B ) -> ( ( z ` x ) e. A <-> ( z ` x ) e. if ( x = y , A , B ) ) )
7		eleq2 2690	. . . . . . . . . . . 12 |- ( B = if ( x = y , A , B ) -> ( ( z ` x ) e. B <-> ( z ` x ) e. if ( x = y , A , B ) ) )
8		simplr 792	. . . . . . . . . . . 12 |- ( ( ( A C_ B /\ ( z ` x ) e. A ) /\ x = y ) -> ( z ` x ) e. A )
9		ssel2 3598	. . . . . . . . . . . . 13 |- ( ( A C_ B /\ ( z ` x ) e. A ) -> ( z ` x ) e. B )
10	9	adantr 481	. . . . . . . . . . . 12 |- ( ( ( A C_ B /\ ( z ` x ) e. A ) /\ -. x = y ) -> ( z ` x ) e. B )
11	6, 7, 8, 10	ifbothda 4123	. . . . . . . . . . 11 |- ( ( A C_ B /\ ( z ` x ) e. A ) -> ( z ` x ) e. if ( x = y , A , B ) )
12	11	ex 450	. . . . . . . . . 10 |- ( A C_ B -> ( ( z ` x ) e. A -> ( z ` x ) e. if ( x = y , A , B ) ) )
13	12	ral2imi 2947	. . . . . . . . 9 |- ( 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 481	. . . . . . . 8 |- ( ( 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 649	. . . . . . 7 |- ( ( 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 554	. . . . . 6 |- ( ( 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 2967	. . . . 5 |- ( ( 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 557	. . . 4 |- ( ( 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 802	. . . . 5 |- ( ( 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 477	. . . . . . . 8 |- ( ( 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 2952	. . . . . . 7 |- ( 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 3098	. . . . . . . 8 |- ( 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 4092	. . . . . . . . . . . 12 |- ( x = y -> if ( x = y , A , B ) = A )
24	23	equcoms 1947	. . . . . . . . . . 11 |- ( y = x -> if ( x = y , A , B ) = A )
25	24	eleq2d 2687	. . . . . . . . . 10 |- ( y = x -> ( ( z ` x ) e. if ( x = y , A , B ) <-> ( z ` x ) e. A ) )
26	25	rspcva 3307	. . . . . . . . 9 |- ( ( x e. I /\ A. y e. I ( z ` x ) e. if ( x = y , A , B ) ) -> ( z ` x ) e. A )
27	26	ralimiaa 2951	. . . . . . . 8 |- ( 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 207	. . . . . . 7 |- ( 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 17	. . . . . 6 |- ( 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 765	. . . . 5 |- ( ( 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 554	. . . 4 |- ( ( 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 877	. . 3 |- ( 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 3203	. . . 4 |- z e. _V
34	33	elixp 7915	. . 3 |- ( z e. X_ x e. I A <-> ( z Fn I /\ A. x e. I ( z ` x ) e. A ) )
35		elin 3796	. . . 4 |- ( 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 7915	. . . . 5 |- ( z e. X_ x e. I B <-> ( z Fn I /\ A. x e. I ( z ` x ) e. B ) )
37		eliin 4525	. . . . . . 7 |- ( 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	33, 37	ax-mp 5	. . . . . 6 |- ( 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 7915	. . . . . . 7 |- ( 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 2980	. . . . . 6 |- ( 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 264	. . . . 5 |- ( 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 733	. . . 4 |- ( ( 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 264	. . 3 |- ( 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 303	. 2 |- ( 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 2620	1 |- ( 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 ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   = wceq 1483   e. wcel 1990   A.wral 2912   _Vcvv 3200   i^i cin 3573   C_ wss 3574   ifcif 4086   |^|_ciin 4521   Fn wfn 5883   ` cfv 5888   X_cixp 7908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-iin 4523  df-br 4654  df-opab 4713  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-iota 5851  df-fun 5890  df-fn 5891  df-fv 5896  df-ixp 7909

This theorem is referenced by:  ptcld  21416  kelac1  37633