Metamath Proof Explorer

Theorem nfcprod

Description: Bound-variable hypothesis builder for product: if x is (effectively) not free in A and B , it is not free in prod_ k e. A B . (Contributed by Scott Fenton, 1-Dec-2017)

Ref Expression
Hypotheses nfcprod.1 
|- F/_ x A
nfcprod.2 
|- F/_ x B
Assertion nfcprod 
|- F/_ x prod_ k e. A B

Proof

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