Metamath Proof Explorer

Theorem fprod2dlem

Description: Lemma for fprod2d - induction step. (Contributed by Scott Fenton, 30-Jan-2018)

Ref Expression
Hypotheses fprod2d.1 
|- ( z = <. j , k >. -> D = C )
fprod2d.2 
|- ( ph -> A e. Fin )
fprod2d.3 
|- ( ( ph /\ j e. A ) -> B e. Fin )
fprod2d.4 
|- ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
fprod2d.5 
|- ( ph -> -. y e. x )
fprod2d.6 
|- ( ph -> ( x u. { y } ) C_ A )
fprod2d.7 
|- ( ps <-> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D )
Assertion fprod2dlem 
|- ( ( ph /\ ps ) -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )

Proof

Step Hyp Ref Expression
1 fprod2d.1 
 |-  ( z = <. j , k >. -> D = C )
2 fprod2d.2 
 |-  ( ph -> A e. Fin )
3 fprod2d.3 
 |-  ( ( ph /\ j e. A ) -> B e. Fin )
4 fprod2d.4 
 |-  ( ( ph /\ ( j e. A /\ k e. B ) ) -> C e. CC )
5 fprod2d.5 
 |-  ( ph -> -. y e. x )
6 fprod2d.6 
 |-  ( ph -> ( x u. { y } ) C_ A )
7 fprod2d.7 
 |-  ( ps <-> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D )
8 7 bilani 
 |-  ( ( ph /\ ps ) -> prod_ j e. x prod_ k e. B C = prod_ z e. U_ j e. x ( { j } X. B ) D )
9 nfcv 
 |-  F/_ m prod_ k e. B C
10 nfcsb1v 
 |-  F/_ j [_ m / j ]_ B
11 nfcsb1v 
 |-  F/_ j [_ m / j ]_ C
12 10 11 nfcprod 
 |-  F/_ j prod_ k e. [_ m / j ]_ B [_ m / j ]_ C
13 csbeq1a 
 |-  ( j = m -> B = [_ m / j ]_ B )
14 csbeq1a 
 |-  ( j = m -> C = [_ m / j ]_ C )
15 14 adantr 
 |-  ( ( j = m /\ k e. B ) -> C = [_ m / j ]_ C )
16 13 15 prodeq12dv 
 |-  ( j = m -> prod_ k e. B C = prod_ k e. [_ m / j ]_ B [_ m / j ]_ C )
17 9 12 16 cbvprodi 
 |-  prod_ j e. { y } prod_ k e. B C = prod_ m e. { y } prod_ k e. [_ m / j ]_ B [_ m / j ]_ C
18 6 unssbd 
 |-  ( ph -> { y } C_ A )
19 vex 
 |-  y e. _V
20 19 snss 
 |-  ( y e. A <-> { y } C_ A )
21 18 20 sylibr 
 |-  ( ph -> y e. A )
22 3 ralrimiva 
 |-  ( ph -> A. j e. A B e. Fin )
23 nfcsb1v 
 |-  F/_ j [_ y / j ]_ B
24 23 nfel1 
 |-  F/ j [_ y / j ]_ B e. Fin
25 csbeq1a 
 |-  ( j = y -> B = [_ y / j ]_ B )
26 25 eleq1d 
 |-  ( j = y -> ( B e. Fin <-> [_ y / j ]_ B e. Fin ) )
27 24 26 rspc 
 |-  ( y e. A -> ( A. j e. A B e. Fin -> [_ y / j ]_ B e. Fin ) )
28 21 22 27 sylc 
 |-  ( ph -> [_ y / j ]_ B e. Fin )
29 4 ralrimivva 
 |-  ( ph -> A. j e. A A. k e. B C e. CC )
30 nfcsb1v 
 |-  F/_ j [_ y / j ]_ C
31 30 nfel1 
 |-  F/ j [_ y / j ]_ C e. CC
32 23 31 nfralw 
 |-  F/ j A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC
33 csbeq1a 
 |-  ( j = y -> C = [_ y / j ]_ C )
34 33 eleq1d 
 |-  ( j = y -> ( C e. CC <-> [_ y / j ]_ C e. CC ) )
35 25 34 raleqbidv 
 |-  ( j = y -> ( A. k e. B C e. CC <-> A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC ) )
36 32 35 rspc 
 |-  ( y e. A -> ( A. j e. A A. k e. B C e. CC -> A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC ) )
37 21 29 36 sylc 
 |-  ( ph -> A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC )
38 37 r19.21bi 
 |-  ( ( ph /\ k e. [_ y / j ]_ B ) -> [_ y / j ]_ C e. CC )
39 28 38 fprodcl 
 |-  ( ph -> prod_ k e. [_ y / j ]_ B [_ y / j ]_ C e. CC )
40 csbeq1 
 |-  ( m = y -> [_ m / j ]_ B = [_ y / j ]_ B )
41 csbeq1 
 |-  ( m = y -> [_ m / j ]_ C = [_ y / j ]_ C )
42 41 adantr 
 |-  ( ( m = y /\ k e. [_ m / j ]_ B ) -> [_ m / j ]_ C = [_ y / j ]_ C )
43 40 42 prodeq12dv 
 |-  ( m = y -> prod_ k e. [_ m / j ]_ B [_ m / j ]_ C = prod_ k e. [_ y / j ]_ B [_ y / j ]_ C )
44 43 prodsn 
 |-  ( ( y e. A /\ prod_ k e. [_ y / j ]_ B [_ y / j ]_ C e. CC ) -> prod_ m e. { y } prod_ k e. [_ m / j ]_ B [_ m / j ]_ C = prod_ k e. [_ y / j ]_ B [_ y / j ]_ C )
45 21 39 44 syl2anc 
 |-  ( ph -> prod_ m e. { y } prod_ k e. [_ m / j ]_ B [_ m / j ]_ C = prod_ k e. [_ y / j ]_ B [_ y / j ]_ C )
46 nfcv 
 |-  F/_ m [_ y / j ]_ C
47 nfcsb1v 
 |-  F/_ k [_ m / k ]_ [_ y / j ]_ C
48 csbeq1a 
 |-  ( k = m -> [_ y / j ]_ C = [_ m / k ]_ [_ y / j ]_ C )
49 46 47 48 cbvprodi 
 |-  prod_ k e. [_ y / j ]_ B [_ y / j ]_ C = prod_ m e. [_ y / j ]_ B [_ m / k ]_ [_ y / j ]_ C
50 csbeq1 
 |-  ( m = ( 2nd ` z ) -> [_ m / k ]_ [_ y / j ]_ C = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
51 snfi 
 |-  { y } e. Fin
52 xpfi 
 |-  ( ( { y } e. Fin /\ [_ y / j ]_ B e. Fin ) -> ( { y } X. [_ y / j ]_ B ) e. Fin )
53 51 28 52 sylancr 
 |-  ( ph -> ( { y } X. [_ y / j ]_ B ) e. Fin )
54 2ndconst 
 |-  ( y e. A -> ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) : ( { y } X. [_ y / j ]_ B ) -1-1-onto-> [_ y / j ]_ B )
55 21 54 syl 
 |-  ( ph -> ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) : ( { y } X. [_ y / j ]_ B ) -1-1-onto-> [_ y / j ]_ B )
56 fvres 
 |-  ( z e. ( { y } X. [_ y / j ]_ B ) -> ( ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) ` z ) = ( 2nd ` z ) )
57 56 adantl 
 |-  ( ( ph /\ z e. ( { y } X. [_ y / j ]_ B ) ) -> ( ( 2nd |` ( { y } X. [_ y / j ]_ B ) ) ` z ) = ( 2nd ` z ) )
58 47 nfel1 
 |-  F/ k [_ m / k ]_ [_ y / j ]_ C e. CC
59 48 eleq1d 
 |-  ( k = m -> ( [_ y / j ]_ C e. CC <-> [_ m / k ]_ [_ y / j ]_ C e. CC ) )
60 58 59 rspc 
 |-  ( m e. [_ y / j ]_ B -> ( A. k e. [_ y / j ]_ B [_ y / j ]_ C e. CC -> [_ m / k ]_ [_ y / j ]_ C e. CC ) )
61 37 60 mpan9 
 |-  ( ( ph /\ m e. [_ y / j ]_ B ) -> [_ m / k ]_ [_ y / j ]_ C e. CC )
62 50 53 55 57 61 fprodf1o 
 |-  ( ph -> prod_ m e. [_ y / j ]_ B [_ m / k ]_ [_ y / j ]_ C = prod_ z e. ( { y } X. [_ y / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
63 elxp 
 |-  ( z e. ( { y } X. [_ y / j ]_ B ) <-> E. m E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) )
64 nfv 
 |-  F/ j z = <. m , k >.
65 nfv 
 |-  F/ j m e. { y }
66 23 nfcri 
 |-  F/ j k e. [_ y / j ]_ B
67 65 66 nfan 
 |-  F/ j ( m e. { y } /\ k e. [_ y / j ]_ B )
68 64 67 nfan 
 |-  F/ j ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) )
69 68 nfex 
 |-  F/ j E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) )
70 nfv 
 |-  F/ m E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) )
71 opeq1 
 |-  ( m = j -> <. m , k >. = <. j , k >. )
72 71 eqeq2d 
 |-  ( m = j -> ( z = <. m , k >. <-> z = <. j , k >. ) )
73 eleq1w 
 |-  ( m = j -> ( m e. { y } <-> j e. { y } ) )
74 velsn 
 |-  ( j e. { y } <-> j = y )
75 73 74 bitrdi 
 |-  ( m = j -> ( m e. { y } <-> j = y ) )
76 75 anbi1d 
 |-  ( m = j -> ( ( m e. { y } /\ k e. [_ y / j ]_ B ) <-> ( j = y /\ k e. [_ y / j ]_ B ) ) )
77 25 eleq2d 
 |-  ( j = y -> ( k e. B <-> k e. [_ y / j ]_ B ) )
78 77 pm5.32i 
 |-  ( ( j = y /\ k e. B ) <-> ( j = y /\ k e. [_ y / j ]_ B ) )
79 76 78 bitr4di 
 |-  ( m = j -> ( ( m e. { y } /\ k e. [_ y / j ]_ B ) <-> ( j = y /\ k e. B ) ) )
80 72 79 anbi12d 
 |-  ( m = j -> ( ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) <-> ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) ) )
81 80 exbidv 
 |-  ( m = j -> ( E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) <-> E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) ) )
82 69 70 81 cbvexv1 
 |-  ( E. m E. k ( z = <. m , k >. /\ ( m e. { y } /\ k e. [_ y / j ]_ B ) ) <-> E. j E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) )
83 63 82 bitri 
 |-  ( z e. ( { y } X. [_ y / j ]_ B ) <-> E. j E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) )
84 nfv 
 |-  F/ j ph
85 nfcv 
 |-  F/_ j ( 2nd ` z )
86 85 30 nfcsbw 
 |-  F/_ j [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
87 86 nfeq2 
 |-  F/ j D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
88 nfv 
 |-  F/ k ph
89 nfcsb1v 
 |-  F/_ k [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
90 89 nfeq2 
 |-  F/ k D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C
91 1 ad2antlr 
 |-  ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> D = C )
92 33 ad2antrl 
 |-  ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> C = [_ y / j ]_ C )
93 fveq2 
 |-  ( z = <. j , k >. -> ( 2nd ` z ) = ( 2nd ` <. j , k >. ) )
94 vex 
 |-  j e. _V
95 vex 
 |-  k e. _V
96 94 95 op2nd 
 |-  ( 2nd ` <. j , k >. ) = k
97 93 96 eqtr2di 
 |-  ( z = <. j , k >. -> k = ( 2nd ` z ) )
98 97 ad2antlr 
 |-  ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> k = ( 2nd ` z ) )
99 csbeq1a 
 |-  ( k = ( 2nd ` z ) -> [_ y / j ]_ C = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
100 98 99 syl 
 |-  ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> [_ y / j ]_ C = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
101 91 92 100 3eqtrd 
 |-  ( ( ( ph /\ z = <. j , k >. ) /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
102 101 expl 
 |-  ( ph -> ( ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
103 88 90 102 exlimd 
 |-  ( ph -> ( E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
104 84 87 103 exlimd 
 |-  ( ph -> ( E. j E. k ( z = <. j , k >. /\ ( j = y /\ k e. B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
105 83 104 biimtrid 
 |-  ( ph -> ( z e. ( { y } X. [_ y / j ]_ B ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C ) )
106 105 imp 
 |-  ( ( ph /\ z e. ( { y } X. [_ y / j ]_ B ) ) -> D = [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
107 106 prodeq2dv 
 |-  ( ph -> prod_ z e. ( { y } X. [_ y / j ]_ B ) D = prod_ z e. ( { y } X. [_ y / j ]_ B ) [_ ( 2nd ` z ) / k ]_ [_ y / j ]_ C )
108 62 107 eqtr4d 
 |-  ( ph -> prod_ m e. [_ y / j ]_ B [_ m / k ]_ [_ y / j ]_ C = prod_ z e. ( { y } X. [_ y / j ]_ B ) D )
109 49 108 eqtrid 
 |-  ( ph -> prod_ k e. [_ y / j ]_ B [_ y / j ]_ C = prod_ z e. ( { y } X. [_ y / j ]_ B ) D )
110 45 109 eqtrd 
 |-  ( ph -> prod_ m e. { y } prod_ k e. [_ m / j ]_ B [_ m / j ]_ C = prod_ z e. ( { y } X. [_ y / j ]_ B ) D )
111 17 110 eqtrid 
 |-  ( ph -> prod_ j e. { y } prod_ k e. B C = prod_ z e. ( { y } X. [_ y / j ]_ B ) D )
112 111 adantr 
 |-  ( ( ph /\ ps ) -> prod_ j e. { y } prod_ k e. B C = prod_ z e. ( { y } X. [_ y / j ]_ B ) D )
113 8 112 oveq12d 
 |-  ( ( ph /\ ps ) -> ( prod_ j e. x prod_ k e. B C x. prod_ j e. { y } prod_ k e. B C ) = ( prod_ z e. U_ j e. x ( { j } X. B ) D x. prod_ z e. ( { y } X. [_ y / j ]_ B ) D ) )
114 disjsn 
 |-  ( ( x i^i { y } ) = (/) <-> -. y e. x )
115 5 114 sylibr 
 |-  ( ph -> ( x i^i { y } ) = (/) )
116 eqidd 
 |-  ( ph -> ( x u. { y } ) = ( x u. { y } ) )
117 2 6 ssfid 
 |-  ( ph -> ( x u. { y } ) e. Fin )
118 6 sselda 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> j e. A )
119 4 anassrs 
 |-  ( ( ( ph /\ j e. A ) /\ k e. B ) -> C e. CC )
120 3 119 fprodcl 
 |-  ( ( ph /\ j e. A ) -> prod_ k e. B C e. CC )
121 118 120 syldan 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> prod_ k e. B C e. CC )
122 115 116 117 121 fprodsplit 
 |-  ( ph -> prod_ j e. ( x u. { y } ) prod_ k e. B C = ( prod_ j e. x prod_ k e. B C x. prod_ j e. { y } prod_ k e. B C ) )
123 122 adantr 
 |-  ( ( ph /\ ps ) -> prod_ j e. ( x u. { y } ) prod_ k e. B C = ( prod_ j e. x prod_ k e. B C x. prod_ j e. { y } prod_ k e. B C ) )
124 eliun 
 |-  ( z e. U_ j e. x ( { j } X. B ) <-> E. j e. x z e. ( { j } X. B ) )
125 xp1st 
 |-  ( z e. ( { j } X. B ) -> ( 1st ` z ) e. { j } )
126 elsni 
 |-  ( ( 1st ` z ) e. { j } -> ( 1st ` z ) = j )
127 125 126 syl 
 |-  ( z e. ( { j } X. B ) -> ( 1st ` z ) = j )
128 127 eleq1d 
 |-  ( z e. ( { j } X. B ) -> ( ( 1st ` z ) e. x <-> j e. x ) )
129 128 biimparc 
 |-  ( ( j e. x /\ z e. ( { j } X. B ) ) -> ( 1st ` z ) e. x )
130 129 rexlimiva 
 |-  ( E. j e. x z e. ( { j } X. B ) -> ( 1st ` z ) e. x )
131 124 130 sylbi 
 |-  ( z e. U_ j e. x ( { j } X. B ) -> ( 1st ` z ) e. x )
132 xp1st 
 |-  ( z e. ( { y } X. [_ y / j ]_ B ) -> ( 1st ` z ) e. { y } )
133 131 132 anim12i 
 |-  ( ( z e. U_ j e. x ( { j } X. B ) /\ z e. ( { y } X. [_ y / j ]_ B ) ) -> ( ( 1st ` z ) e. x /\ ( 1st ` z ) e. { y } ) )
134 elin 
 |-  ( z e. ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) <-> ( z e. U_ j e. x ( { j } X. B ) /\ z e. ( { y } X. [_ y / j ]_ B ) ) )
135 elin 
 |-  ( ( 1st ` z ) e. ( x i^i { y } ) <-> ( ( 1st ` z ) e. x /\ ( 1st ` z ) e. { y } ) )
136 133 134 135 3imtr4i 
 |-  ( z e. ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) -> ( 1st ` z ) e. ( x i^i { y } ) )
137 115 eleq2d 
 |-  ( ph -> ( ( 1st ` z ) e. ( x i^i { y } ) <-> ( 1st ` z ) e. (/) ) )
138 noel 
 |-  -. ( 1st ` z ) e. (/)
139 138 pm2.21i 
 |-  ( ( 1st ` z ) e. (/) -> z e. (/) )
140 137 139 biimtrdi 
 |-  ( ph -> ( ( 1st ` z ) e. ( x i^i { y } ) -> z e. (/) ) )
141 136 140 syl5 
 |-  ( ph -> ( z e. ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) -> z e. (/) ) )
142 141 ssrdv 
 |-  ( ph -> ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) C_ (/) )
143 ss0 
 |-  ( ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) C_ (/) -> ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) = (/) )
144 142 143 syl 
 |-  ( ph -> ( U_ j e. x ( { j } X. B ) i^i ( { y } X. [_ y / j ]_ B ) ) = (/) )
145 iunxun 
 |-  U_ j e. ( x u. { y } ) ( { j } X. B ) = ( U_ j e. x ( { j } X. B ) u. U_ j e. { y } ( { j } X. B ) )
146 nfcv 
 |-  F/_ m ( { j } X. B )
147 nfcv 
 |-  F/_ j { m }
148 147 10 nfxp 
 |-  F/_ j ( { m } X. [_ m / j ]_ B )
149 sneq 
 |-  ( j = m -> { j } = { m } )
150 149 13 xpeq12d 
 |-  ( j = m -> ( { j } X. B ) = ( { m } X. [_ m / j ]_ B ) )
151 146 148 150 cbviun 
 |-  U_ j e. { y } ( { j } X. B ) = U_ m e. { y } ( { m } X. [_ m / j ]_ B )
152 sneq 
 |-  ( m = y -> { m } = { y } )
153 152 40 xpeq12d 
 |-  ( m = y -> ( { m } X. [_ m / j ]_ B ) = ( { y } X. [_ y / j ]_ B ) )
154 19 153 iunxsn 
 |-  U_ m e. { y } ( { m } X. [_ m / j ]_ B ) = ( { y } X. [_ y / j ]_ B )
155 151 154 eqtri 
 |-  U_ j e. { y } ( { j } X. B ) = ( { y } X. [_ y / j ]_ B )
156 155 uneq2i 
 |-  ( U_ j e. x ( { j } X. B ) u. U_ j e. { y } ( { j } X. B ) ) = ( U_ j e. x ( { j } X. B ) u. ( { y } X. [_ y / j ]_ B ) )
157 145 156 eqtri 
 |-  U_ j e. ( x u. { y } ) ( { j } X. B ) = ( U_ j e. x ( { j } X. B ) u. ( { y } X. [_ y / j ]_ B ) )
158 157 a1i 
 |-  ( ph -> U_ j e. ( x u. { y } ) ( { j } X. B ) = ( U_ j e. x ( { j } X. B ) u. ( { y } X. [_ y / j ]_ B ) ) )
159 snfi 
 |-  { j } e. Fin
160 118 3 syldan 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> B e. Fin )
161 xpfi 
 |-  ( ( { j } e. Fin /\ B e. Fin ) -> ( { j } X. B ) e. Fin )
162 159 160 161 sylancr 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> ( { j } X. B ) e. Fin )
163 162 ralrimiva 
 |-  ( ph -> A. j e. ( x u. { y } ) ( { j } X. B ) e. Fin )
164 iunfi 
 |-  ( ( ( x u. { y } ) e. Fin /\ A. j e. ( x u. { y } ) ( { j } X. B ) e. Fin ) -> U_ j e. ( x u. { y } ) ( { j } X. B ) e. Fin )
165 117 163 164 syl2anc 
 |-  ( ph -> U_ j e. ( x u. { y } ) ( { j } X. B ) e. Fin )
166 eliun 
 |-  ( z e. U_ j e. ( x u. { y } ) ( { j } X. B ) <-> E. j e. ( x u. { y } ) z e. ( { j } X. B ) )
167 elxp 
 |-  ( z e. ( { j } X. B ) <-> E. m E. k ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) )
168 simprl 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> z = <. m , k >. )
169 simprrl 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> m e. { j } )
170 elsni 
 |-  ( m e. { j } -> m = j )
171 169 170 syl 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> m = j )
172 171 opeq1d 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> <. m , k >. = <. j , k >. )
173 168 172 eqtrd 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> z = <. j , k >. )
174 173 1 syl 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> D = C )
175 simpll 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> ph )
176 118 adantr 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> j e. A )
177 simprrr 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> k e. B )
178 175 176 177 4 syl12anc 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> C e. CC )
179 174 178 eqeltrd 
 |-  ( ( ( ph /\ j e. ( x u. { y } ) ) /\ ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) ) -> D e. CC )
180 179 ex 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> ( ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) -> D e. CC ) )
181 180 exlimdvv 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> ( E. m E. k ( z = <. m , k >. /\ ( m e. { j } /\ k e. B ) ) -> D e. CC ) )
182 167 181 biimtrid 
 |-  ( ( ph /\ j e. ( x u. { y } ) ) -> ( z e. ( { j } X. B ) -> D e. CC ) )
183 182 rexlimdva 
 |-  ( ph -> ( E. j e. ( x u. { y } ) z e. ( { j } X. B ) -> D e. CC ) )
184 166 183 biimtrid 
 |-  ( ph -> ( z e. U_ j e. ( x u. { y } ) ( { j } X. B ) -> D e. CC ) )
185 184 imp 
 |-  ( ( ph /\ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) ) -> D e. CC )
186 144 158 165 185 fprodsplit 
 |-  ( ph -> prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D = ( prod_ z e. U_ j e. x ( { j } X. B ) D x. prod_ z e. ( { y } X. [_ y / j ]_ B ) D ) )
187 186 adantr 
 |-  ( ( ph /\ ps ) -> prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D = ( prod_ z e. U_ j e. x ( { j } X. B ) D x. prod_ z e. ( { y } X. [_ y / j ]_ B ) D ) )
188 113 123 187 3eqtr4d 
 |-  ( ( ph /\ ps ) -> prod_ j e. ( x u. { y } ) prod_ k e. B C = prod_ z e. U_ j e. ( x u. { y } ) ( { j } X. B ) D )