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