# Metamath Proof Explorer

## Theorem fprod

Description: The value of a product over a nonempty finite set. (Contributed by Scott Fenton, 6-Dec-2017)

Ref Expression
Hypotheses fprod.1
`|- ( k = ( F ` n ) -> B = C )`
fprod.2
`|- ( ph -> M e. NN )`
fprod.3
`|- ( ph -> F : ( 1 ... M ) -1-1-onto-> A )`
fprod.4
`|- ( ( ph /\ k e. A ) -> B e. CC )`
fprod.5
`|- ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = C )`
Assertion fprod
`|- ( ph -> prod_ k e. A B = ( seq 1 ( x. , G ) ` M ) )`

### Proof

Step Hyp Ref Expression
1 fprod.1
` |-  ( k = ( F ` n ) -> B = C )`
2 fprod.2
` |-  ( ph -> M e. NN )`
3 fprod.3
` |-  ( ph -> F : ( 1 ... M ) -1-1-onto-> A )`
4 fprod.4
` |-  ( ( ph /\ k e. A ) -> B e. CC )`
5 fprod.5
` |-  ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = C )`
6 df-prod
` |-  prod_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )`
7 fvex
` |-  ( seq 1 ( x. , G ) ` M ) e. _V`
8 nfcv
` |-  F/_ j if ( k e. A , B , 1 )`
9 nfv
` |-  F/ k j e. A`
10 nfcsb1v
` |-  F/_ k [_ j / k ]_ B`
11 nfcv
` |-  F/_ k 1`
12 9 10 11 nfif
` |-  F/_ k if ( j e. A , [_ j / k ]_ B , 1 )`
13 eleq1w
` |-  ( k = j -> ( k e. A <-> j e. A ) )`
14 csbeq1a
` |-  ( k = j -> B = [_ j / k ]_ B )`
15 13 14 ifbieq1d
` |-  ( k = j -> if ( k e. A , B , 1 ) = if ( j e. A , [_ j / k ]_ B , 1 ) )`
16 8 12 15 cbvmpt
` |-  ( k e. ZZ |-> if ( k e. A , B , 1 ) ) = ( j e. ZZ |-> if ( j e. A , [_ j / k ]_ B , 1 ) )`
17 4 ralrimiva
` |-  ( ph -> A. k e. A B e. CC )`
18 10 nfel1
` |-  F/ k [_ j / k ]_ B e. CC`
19 14 eleq1d
` |-  ( k = j -> ( B e. CC <-> [_ j / k ]_ B e. CC ) )`
20 18 19 rspc
` |-  ( j e. A -> ( A. k e. A B e. CC -> [_ j / k ]_ B e. CC ) )`
21 17 20 mpan9
` |-  ( ( ph /\ j e. A ) -> [_ j / k ]_ B e. CC )`
22 fveq2
` |-  ( n = i -> ( f ` n ) = ( f ` i ) )`
23 22 csbeq1d
` |-  ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / k ]_ B )`
24 csbcow
` |-  [_ ( f ` i ) / j ]_ [_ j / k ]_ B = [_ ( f ` i ) / k ]_ B`
25 23 24 eqtr4di
` |-  ( n = i -> [_ ( f ` n ) / k ]_ B = [_ ( f ` i ) / j ]_ [_ j / k ]_ B )`
26 25 cbvmptv
` |-  ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( i e. NN |-> [_ ( f ` i ) / j ]_ [_ j / k ]_ B )`
27 16 21 26 prodmo
` |-  ( ph -> E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )`
28 f1of
` |-  ( F : ( 1 ... M ) -1-1-onto-> A -> F : ( 1 ... M ) --> A )`
29 3 28 syl
` |-  ( ph -> F : ( 1 ... M ) --> A )`
30 ovex
` |-  ( 1 ... M ) e. _V`
31 fex
` |-  ( ( F : ( 1 ... M ) --> A /\ ( 1 ... M ) e. _V ) -> F e. _V )`
32 29 30 31 sylancl
` |-  ( ph -> F e. _V )`
33 nnuz
` |-  NN = ( ZZ>= ` 1 )`
34 2 33 eleqtrdi
` |-  ( ph -> M e. ( ZZ>= ` 1 ) )`
35 elfznn
` |-  ( n e. ( 1 ... M ) -> n e. NN )`
36 fvex
` |-  ( G ` n ) e. _V`
37 5 36 eqeltrrdi
` |-  ( ( ph /\ n e. ( 1 ... M ) ) -> C e. _V )`
38 eqid
` |-  ( n e. NN |-> C ) = ( n e. NN |-> C )`
39 38 fvmpt2
` |-  ( ( n e. NN /\ C e. _V ) -> ( ( n e. NN |-> C ) ` n ) = C )`
40 35 37 39 syl2an2
` |-  ( ( ph /\ n e. ( 1 ... M ) ) -> ( ( n e. NN |-> C ) ` n ) = C )`
41 5 40 eqtr4d
` |-  ( ( ph /\ n e. ( 1 ... M ) ) -> ( G ` n ) = ( ( n e. NN |-> C ) ` n ) )`
42 41 ralrimiva
` |-  ( ph -> A. n e. ( 1 ... M ) ( G ` n ) = ( ( n e. NN |-> C ) ` n ) )`
43 nffvmpt1
` |-  F/_ n ( ( n e. NN |-> C ) ` k )`
44 43 nfeq2
` |-  F/ n ( G ` k ) = ( ( n e. NN |-> C ) ` k )`
45 fveq2
` |-  ( n = k -> ( G ` n ) = ( G ` k ) )`
46 fveq2
` |-  ( n = k -> ( ( n e. NN |-> C ) ` n ) = ( ( n e. NN |-> C ) ` k ) )`
47 45 46 eqeq12d
` |-  ( n = k -> ( ( G ` n ) = ( ( n e. NN |-> C ) ` n ) <-> ( G ` k ) = ( ( n e. NN |-> C ) ` k ) ) )`
48 44 47 rspc
` |-  ( k e. ( 1 ... M ) -> ( A. n e. ( 1 ... M ) ( G ` n ) = ( ( n e. NN |-> C ) ` n ) -> ( G ` k ) = ( ( n e. NN |-> C ) ` k ) ) )`
49 42 48 mpan9
` |-  ( ( ph /\ k e. ( 1 ... M ) ) -> ( G ` k ) = ( ( n e. NN |-> C ) ` k ) )`
50 34 49 seqfveq
` |-  ( ph -> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> C ) ) ` M ) )`
51 3 50 jca
` |-  ( ph -> ( F : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> C ) ) ` M ) ) )`
52 f1oeq1
` |-  ( f = F -> ( f : ( 1 ... M ) -1-1-onto-> A <-> F : ( 1 ... M ) -1-1-onto-> A ) )`
53 fveq1
` |-  ( f = F -> ( f ` n ) = ( F ` n ) )`
54 53 csbeq1d
` |-  ( f = F -> [_ ( f ` n ) / k ]_ B = [_ ( F ` n ) / k ]_ B )`
55 fvex
` |-  ( F ` n ) e. _V`
56 55 1 csbie
` |-  [_ ( F ` n ) / k ]_ B = C`
57 54 56 eqtrdi
` |-  ( f = F -> [_ ( f ` n ) / k ]_ B = C )`
58 57 mpteq2dv
` |-  ( f = F -> ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) = ( n e. NN |-> C ) )`
59 58 seqeq3d
` |-  ( f = F -> seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) = seq 1 ( x. , ( n e. NN |-> C ) ) )`
60 59 fveq1d
` |-  ( f = F -> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> C ) ) ` M ) )`
61 60 eqeq2d
` |-  ( f = F -> ( ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) <-> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> C ) ) ` M ) ) )`
62 52 61 anbi12d
` |-  ( f = F -> ( ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) <-> ( F : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> C ) ) ` M ) ) ) )`
63 32 51 62 spcedv
` |-  ( ph -> E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) )`
64 oveq2
` |-  ( m = M -> ( 1 ... m ) = ( 1 ... M ) )`
65 64 f1oeq2d
` |-  ( m = M -> ( f : ( 1 ... m ) -1-1-onto-> A <-> f : ( 1 ... M ) -1-1-onto-> A ) )`
66 fveq2
` |-  ( m = M -> ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) )`
67 66 eqeq2d
` |-  ( m = M -> ( ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) <-> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) )`
68 65 67 anbi12d
` |-  ( m = M -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) ) )`
69 68 exbidv
` |-  ( m = M -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) ) )`
70 69 rspcev
` |-  ( ( M e. NN /\ E. f ( f : ( 1 ... M ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` M ) ) ) -> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )`
71 2 63 70 syl2anc
` |-  ( ph -> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )`
72 71 olcd
` |-  ( ph -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )`
73 breq2
` |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x <-> seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) )`
74 73 3anbi3d
` |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) <-> ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) ) )`
75 74 rexbidv
` |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) <-> E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) ) )`
76 eqeq1
` |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) <-> ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )`
77 76 anbi2d
` |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )`
78 77 exbidv
` |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )`
79 78 rexbidv
` |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) <-> E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )`
80 75 79 orbi12d
` |-  ( x = ( seq 1 ( x. , G ) ` M ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) )`
81 80 moi2
` |-  ( ( ( ( seq 1 ( x. , G ) ` M ) e. _V /\ E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) /\ ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) ) -> x = ( seq 1 ( x. , G ) ` M ) )`
82 7 81 mpanl1
` |-  ( ( E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) ) -> x = ( seq 1 ( x. , G ) ` M ) )`
83 82 ancom2s
` |-  ( ( E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) ) -> x = ( seq 1 ( x. , G ) ` M ) )`
84 83 expr
` |-  ( ( E* x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) /\ ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> ( seq 1 ( x. , G ) ` M ) ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ ( seq 1 ( x. , G ) ` M ) = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) -> x = ( seq 1 ( x. , G ) ` M ) ) )`
85 27 72 84 syl2anc
` |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) -> x = ( seq 1 ( x. , G ) ` M ) ) )`
86 72 80 syl5ibrcom
` |-  ( ph -> ( x = ( seq 1 ( x. , G ) ` M ) -> ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) )`
87 85 86 impbid
` |-  ( ph -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> x = ( seq 1 ( x. , G ) ` M ) ) )`
` |-  ( ( ph /\ ( seq 1 ( x. , G ) ` M ) e. _V ) -> ( ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) <-> x = ( seq 1 ( x. , G ) ` M ) ) )`
` |-  ( ( ph /\ ( seq 1 ( x. , G ) ` M ) e. _V ) -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) = ( seq 1 ( x. , G ) ` M ) )`
` |-  ( ph -> ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y ) /\ seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) ) = ( seq 1 ( x. , G ) ` M ) )`
` |-  ( ph -> prod_ k e. A B = ( seq 1 ( x. , G ) ` M ) )`