Metamath Proof Explorer

Theorem nfsum1

Description: Bound-variable hypothesis builder for sum. (Contributed by NM, 11-Dec-2005) (Revised by Mario Carneiro, 13-Jun-2019)

Ref Expression
Hypothesis nfsum1.1 
|- F/_ k A
Assertion nfsum1 
|- F/_ k sum_ k e. A B

Proof

Step Hyp Ref Expression
1 nfsum1.1 
 |-  F/_ k A
2 df-sum 
 |-  sum_ k e. A B = ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( 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 nfcv 
 |-  F/_ k m
7 nfcv 
 |-  F/_ k +
8 1 nfcri 
 |-  F/ k n e. A
9 nfcsb1v 
 |-  F/_ k [_ n / k ]_ B
10 nfcv 
 |-  F/_ k 0
11 8 9 10 nfif 
 |-  F/_ k if ( n e. A , [_ n / k ]_ B , 0 )
12 3 11 nfmpt 
 |-  F/_ k ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) )
13 6 7 12 nfseq 
 |-  F/_ k seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) )
14 nfcv 
 |-  F/_ k ~~>
15 nfcv 
 |-  F/_ k x
16 13 14 15 nfbr 
 |-  F/ k seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x
17 5 16 nfan 
 |-  F/ k ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x )
18 3 17 nfrexw 
 |-  F/ k E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x )
19 nfcv 
 |-  F/_ k NN
20 nfcv 
 |-  F/_ k f
21 nfcv 
 |-  F/_ k ( 1 ... m )
22 20 21 1 nff1o 
 |-  F/ k f : ( 1 ... m ) -1-1-onto-> A
23 nfcv 
 |-  F/_ k 1
24 nfcsb1v 
 |-  F/_ k [_ ( f ` n ) / k ]_ B
25 19 24 nfmpt 
 |-  F/_ k ( n e. NN |-> [_ ( f ` n ) / k ]_ B )
26 23 7 25 nfseq 
 |-  F/_ k seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) )
27 26 6 nffv 
 |-  F/_ k ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
28 27 nfeq2 
 |-  F/ k x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m )
29 22 28 nfan 
 |-  F/ k ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
30 29 nfex 
 |-  F/ k E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
31 19 30 nfrexw 
 |-  F/ k E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) )
32 18 31 nfor 
 |-  F/ k ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) )
33 32 nfiotaw 
 |-  F/_ k ( iota x ( E. m e. ZZ ( A C_ ( ZZ>= ` m ) /\ seq m ( + , ( n e. ZZ |-> if ( n e. A , [_ n / k ]_ B , 0 ) ) ) ~~> x ) \/ E. m e. NN E. f ( f : ( 1 ... m ) -1-1-onto-> A /\ x = ( seq 1 ( + , ( n e. NN |-> [_ ( f ` n ) / k ]_ B ) ) ` m ) ) ) )
34 2 33 nfcxfr 
 |-  F/_ k sum_ k e. A B