Step |
Hyp |
Ref |
Expression |
1 |
|
dprdff.w |
|- W = { h e. X_ i e. I ( S ` i ) | h finSupp .0. } |
2 |
|
dprdff.1 |
|- ( ph -> G dom DProd S ) |
3 |
|
dprdff.2 |
|- ( ph -> dom S = I ) |
4 |
|
dprdff.3 |
|- ( ph -> F e. W ) |
5 |
1 2 3
|
dprdw |
|- ( ph -> ( F e. W <-> ( F Fn I /\ A. x e. I ( F ` x ) e. ( S ` x ) /\ F finSupp .0. ) ) ) |
6 |
4 5
|
mpbid |
|- ( ph -> ( F Fn I /\ A. x e. I ( F ` x ) e. ( S ` x ) /\ F finSupp .0. ) ) |
7 |
6
|
simp2d |
|- ( ph -> A. x e. I ( F ` x ) e. ( S ` x ) ) |
8 |
|
fveq2 |
|- ( x = X -> ( F ` x ) = ( F ` X ) ) |
9 |
|
fveq2 |
|- ( x = X -> ( S ` x ) = ( S ` X ) ) |
10 |
8 9
|
eleq12d |
|- ( x = X -> ( ( F ` x ) e. ( S ` x ) <-> ( F ` X ) e. ( S ` X ) ) ) |
11 |
10
|
rspccva |
|- ( ( A. x e. I ( F ` x ) e. ( S ` x ) /\ X e. I ) -> ( F ` X ) e. ( S ` X ) ) |
12 |
7 11
|
sylan |
|- ( ( ph /\ X e. I ) -> ( F ` X ) e. ( S ` X ) ) |