Metamath Proof Explorer

Theorem nfcprod1

Description: Bound-variable hypothesis builder for product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypothesis nfcprod1.1 
|- F/_ k A
Assertion nfcprod1 
|- F/_ k prod_ k e. A B

Proof

Step Hyp Ref Expression
1 nfcprod1.1 
 |-  F/_ k A
2 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 ) ) ) )
3 nfcv 
 |-  F/_ k ZZ
4 nfcv 
 |-  F/_ k ( ZZ>= ` m )
5 1 4 nfss 
 |-  F/ k A C_ ( ZZ>= ` m )
6 nfv 
 |-  F/ k y =/= 0
7 nfcv 
 |-  F/_ k n
8 nfcv 
 |-  F/_ k x.
9 nfmpt1 
 |-  F/_ k ( k e. ZZ |-> if ( k e. A , B , 1 ) )
10 7 8 9 nfseq 
 |-  F/_ k seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) )
11 nfcv 
 |-  F/_ k ~~>
12 nfcv 
 |-  F/_ k y
13 10 11 12 nfbr 
 |-  F/ k seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y
14 6 13 nfan 
 |-  F/ k ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
15 14 nfex 
 |-  F/ k E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
16 4 15 nfrex 
 |-  F/ k E. n e. ( ZZ>= ` m ) E. y ( y =/= 0 /\ seq n ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> y )
17 nfcv 
 |-  F/_ k m
18 17 8 9 nfseq 
 |-  F/_ k seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) )
19 nfcv 
 |-  F/_ k x
20 18 11 19 nfbr 
 |-  F/ k seq m ( x. , ( k e. ZZ |-> if ( k e. A , B , 1 ) ) ) ~~> x
21 5 16 20 nf3an 
 |-  F/ k ( 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 )
22 3 21 nfrex 
 |-  F/ k 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 )
23 nfcv 
 |-  F/_ k NN
24 nfcv 
 |-  F/_ k f
25 nfcv 
 |-  F/_ k ( 1 ... m )
26 24 25 1 nff1o 
 |-  F/ k f : ( 1 ... m ) -1-1-onto-> A
27 nfcv 
 |-  F/_ k 1
28 nfcsb1v 
 |-  F/_ k [_ ( f ` n ) / k ]_ B
29 23 28 nfmpt 
 |-  F/_ k ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
30 27 8 29 nfseq 
 |-  F/_ k seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) )
31 30 17 nffv 
 |-  F/_ k ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
32 31 nfeq2 
 |-  F/ k x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
33 26 32 nfan 
 |-  F/ k ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
34 33 nfex 
 |-  F/ k E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( x. , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
35 23 34 nfrex 
 |-  F/ k 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 ) )
36 22 35 nfor 
 |-  F/ k ( 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 ) ) )
37 36 nfiotaw 
 |-  F/_ k ( 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 ) ) ) )
38 2 37 nfcxfr 
 |-  F/_ k prod_ k e. A B