Metamath Proof Explorer

Theorem sticksstones22

Description: Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024)

Ref Expression
Hypotheses sticksstones22.1 
|- ( ph -> N e. NN0 )
sticksstones22.2 
|- ( ph -> S e. Fin )
sticksstones22.3 
|- ( ph -> S =/= (/) )
sticksstones22.4 
|- A = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) }
Assertion sticksstones22 
|- ( ph -> ( # ` A ) = ( ( N + ( # ` S ) ) _C ( # ` S ) ) )

Proof

Step Hyp Ref Expression
1 sticksstones22.1 
 |-  ( ph -> N e. NN0 )
2 sticksstones22.2 
 |-  ( ph -> S e. Fin )
3 sticksstones22.3 
 |-  ( ph -> S =/= (/) )
4 sticksstones22.4 
 |-  A = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) }
5 4 a1i 
 |-  ( ph -> A = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } )
6 5 fveq2d 
 |-  ( ph -> ( # ` A ) = ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } ) )
7 breq2 
 |-  ( x = 0 -> ( sum_ i e. S ( f ` i ) <_ x <-> sum_ i e. S ( f ` i ) <_ 0 ) )
8 7 anbi2d 
 |-  ( x = 0 -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) <-> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) )
9 8 abbidv 
 |-  ( x = 0 -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) } )
10 9 fveq2d 
 |-  ( x = 0 -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } ) = ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) } ) )
11 oveq1 
 |-  ( x = 0 -> ( x + ( # ` S ) ) = ( 0 + ( # ` S ) ) )
12 11 oveq1d 
 |-  ( x = 0 -> ( ( x + ( # ` S ) ) _C ( # ` S ) ) = ( ( 0 + ( # ` S ) ) _C ( # ` S ) ) )
13 10 12 eqeq12d 
 |-  ( x = 0 -> ( ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } ) = ( ( x + ( # ` S ) ) _C ( # ` S ) ) <-> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) } ) = ( ( 0 + ( # ` S ) ) _C ( # ` S ) ) ) )
14 breq2 
 |-  ( x = y -> ( sum_ i e. S ( f ` i ) <_ x <-> sum_ i e. S ( f ` i ) <_ y ) )
15 14 anbi2d 
 |-  ( x = y -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) <-> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) )
16 15 abbidv 
 |-  ( x = y -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } )
17 16 fveq2d 
 |-  ( x = y -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } ) = ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) )
18 oveq1 
 |-  ( x = y -> ( x + ( # ` S ) ) = ( y + ( # ` S ) ) )
19 18 oveq1d 
 |-  ( x = y -> ( ( x + ( # ` S ) ) _C ( # ` S ) ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) )
20 17 19 eqeq12d 
 |-  ( x = y -> ( ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } ) = ( ( x + ( # ` S ) ) _C ( # ` S ) ) <-> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) )
21 breq2 
 |-  ( x = ( y + 1 ) -> ( sum_ i e. S ( f ` i ) <_ x <-> sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) )
22 21 anbi2d 
 |-  ( x = ( y + 1 ) -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) <-> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) )
23 22 abbidv 
 |-  ( x = ( y + 1 ) -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) } )
24 23 fveq2d 
 |-  ( x = ( y + 1 ) -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } ) = ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) } ) )
25 oveq1 
 |-  ( x = ( y + 1 ) -> ( x + ( # ` S ) ) = ( ( y + 1 ) + ( # ` S ) ) )
26 25 oveq1d 
 |-  ( x = ( y + 1 ) -> ( ( x + ( # ` S ) ) _C ( # ` S ) ) = ( ( ( y + 1 ) + ( # ` S ) ) _C ( # ` S ) ) )
27 24 26 eqeq12d 
 |-  ( x = ( y + 1 ) -> ( ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } ) = ( ( x + ( # ` S ) ) _C ( # ` S ) ) <-> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) } ) = ( ( ( y + 1 ) + ( # ` S ) ) _C ( # ` S ) ) ) )
28 breq2 
 |-  ( x = N -> ( sum_ i e. S ( f ` i ) <_ x <-> sum_ i e. S ( f ` i ) <_ N ) )
29 28 anbi2d 
 |-  ( x = N -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) <-> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) ) )
30 29 abbidv 
 |-  ( x = N -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } )
31 30 fveq2d 
 |-  ( x = N -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } ) = ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } ) )
32 oveq1 
 |-  ( x = N -> ( x + ( # ` S ) ) = ( N + ( # ` S ) ) )
33 32 oveq1d 
 |-  ( x = N -> ( ( x + ( # ` S ) ) _C ( # ` S ) ) = ( ( N + ( # ` S ) ) _C ( # ` S ) ) )
34 31 33 eqeq12d 
 |-  ( x = N -> ( ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ x ) } ) = ( ( x + ( # ` S ) ) _C ( # ` S ) ) <-> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } ) = ( ( N + ( # ` S ) ) _C ( # ` S ) ) ) )
35 simprl 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> f : S --> NN0 )
36 simprr 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> sum_ i e. S ( f ` i ) <_ 0 )
37 2 adantr 
 |-  ( ( ph /\ f : S --> NN0 ) -> S e. Fin )
38 simpr 
 |-  ( ( ph /\ f : S --> NN0 ) -> f : S --> NN0 )
39 38 ffvelcdmda 
 |-  ( ( ( ph /\ f : S --> NN0 ) /\ i e. S ) -> ( f ` i ) e. NN0 )
40 37 39 fsumnn0cl 
 |-  ( ( ph /\ f : S --> NN0 ) -> sum_ i e. S ( f ` i ) e. NN0 )
41 35 40 syldan 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> sum_ i e. S ( f ` i ) e. NN0 )
42 41 nn0ge0d 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> 0 <_ sum_ i e. S ( f ` i ) )
43 0red 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> 0 e. RR )
44 41 nn0red 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> sum_ i e. S ( f ` i ) e. RR )
45 43 44 lenltd 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> ( 0 <_ sum_ i e. S ( f ` i ) <-> -. sum_ i e. S ( f ` i ) < 0 ) )
46 42 45 mpbid 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> -. sum_ i e. S ( f ` i ) < 0 )
47 36 46 jca 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> ( sum_ i e. S ( f ` i ) <_ 0 /\ -. sum_ i e. S ( f ` i ) < 0 ) )
48 44 43 eqleltd 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> ( sum_ i e. S ( f ` i ) = 0 <-> ( sum_ i e. S ( f ` i ) <_ 0 /\ -. sum_ i e. S ( f ` i ) < 0 ) ) )
49 47 48 mpbird 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> sum_ i e. S ( f ` i ) = 0 )
50 35 49 jca 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) -> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) )
51 50 ex 
 |-  ( ph -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) -> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) ) )
52 simprl 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) ) -> f : S --> NN0 )
53 simprr 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) ) -> sum_ i e. S ( f ` i ) = 0 )
54 0red 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) ) -> 0 e. RR )
55 54 leidd 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) ) -> 0 <_ 0 )
56 53 55 eqbrtrd 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) ) -> sum_ i e. S ( f ` i ) <_ 0 )
57 52 56 jca 
 |-  ( ( ph /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) ) -> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) )
58 57 ex 
 |-  ( ph -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) -> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) ) )
59 51 58 impbid 
 |-  ( ph -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) <-> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) ) )
60 59 abbidv 
 |-  ( ph -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) } = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) } )
61 60 fveq2d 
 |-  ( ph -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) } ) = ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) } ) )
62 0nn0 
 |-  0 e. NN0
63 62 a1i 
 |-  ( ph -> 0 e. NN0 )
64 eqid 
 |-  { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) } = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) }
65 63 2 3 64 sticksstones21 
 |-  ( ph -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) } ) = ( ( 0 + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) )
66 hashnncl 
 |-  ( S e. Fin -> ( ( # ` S ) e. NN <-> S =/= (/) ) )
67 2 66 syl 
 |-  ( ph -> ( ( # ` S ) e. NN <-> S =/= (/) ) )
68 67 bicomd 
 |-  ( ph -> ( S =/= (/) <-> ( # ` S ) e. NN ) )
69 68 biimpd 
 |-  ( ph -> ( S =/= (/) -> ( # ` S ) e. NN ) )
70 3 69 mpd 
 |-  ( ph -> ( # ` S ) e. NN )
71 70 nncnd 
 |-  ( ph -> ( # ` S ) e. CC )
72 1cnd 
 |-  ( ph -> 1 e. CC )
73 71 72 subcld 
 |-  ( ph -> ( ( # ` S ) - 1 ) e. CC )
74 73 addlidd 
 |-  ( ph -> ( 0 + ( ( # ` S ) - 1 ) ) = ( ( # ` S ) - 1 ) )
75 74 oveq1d 
 |-  ( ph -> ( ( 0 + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) = ( ( ( # ` S ) - 1 ) _C ( ( # ` S ) - 1 ) ) )
76 nnm1nn0 
 |-  ( ( # ` S ) e. NN -> ( ( # ` S ) - 1 ) e. NN0 )
77 70 76 syl 
 |-  ( ph -> ( ( # ` S ) - 1 ) e. NN0 )
78 bcnn 
 |-  ( ( ( # ` S ) - 1 ) e. NN0 -> ( ( ( # ` S ) - 1 ) _C ( ( # ` S ) - 1 ) ) = 1 )
79 77 78 syl 
 |-  ( ph -> ( ( ( # ` S ) - 1 ) _C ( ( # ` S ) - 1 ) ) = 1 )
80 75 79 eqtrd 
 |-  ( ph -> ( ( 0 + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) = 1 )
81 eqidd 
 |-  ( ph -> 1 = 1 )
82 70 nnnn0d 
 |-  ( ph -> ( # ` S ) e. NN0 )
83 bcnn 
 |-  ( ( # ` S ) e. NN0 -> ( ( # ` S ) _C ( # ` S ) ) = 1 )
84 82 83 syl 
 |-  ( ph -> ( ( # ` S ) _C ( # ` S ) ) = 1 )
85 84 eqcomd 
 |-  ( ph -> 1 = ( ( # ` S ) _C ( # ` S ) ) )
86 71 addlidd 
 |-  ( ph -> ( 0 + ( # ` S ) ) = ( # ` S ) )
87 86 eqcomd 
 |-  ( ph -> ( # ` S ) = ( 0 + ( # ` S ) ) )
88 87 oveq1d 
 |-  ( ph -> ( ( # ` S ) _C ( # ` S ) ) = ( ( 0 + ( # ` S ) ) _C ( # ` S ) ) )
89 85 88 eqtrd 
 |-  ( ph -> 1 = ( ( 0 + ( # ` S ) ) _C ( # ` S ) ) )
90 80 81 89 3eqtrd 
 |-  ( ph -> ( ( 0 + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) = ( ( 0 + ( # ` S ) ) _C ( # ` S ) ) )
91 65 90 eqtrd 
 |-  ( ph -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = 0 ) } ) = ( ( 0 + ( # ` S ) ) _C ( # ` S ) ) )
92 61 91 eqtrd 
 |-  ( ph -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ 0 ) } ) = ( ( 0 + ( # ` S ) ) _C ( # ` S ) ) )
93 simprl 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> f : S --> NN0 )
94 simprr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> sum_ i e. S ( f ` i ) <_ ( y + 1 ) )
95 2 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) -> S e. Fin )
96 simpr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) -> f : S --> NN0 )
97 96 ffvelcdmda 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) /\ i e. S ) -> ( f ` i ) e. NN0 )
98 95 97 fsumnn0cl 
 |-  ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) -> sum_ i e. S ( f ` i ) e. NN0 )
99 93 98 syldan 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> sum_ i e. S ( f ` i ) e. NN0 )
100 99 nn0red 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> sum_ i e. S ( f ` i ) e. RR )
101 nn0re 
 |-  ( y e. NN0 -> y e. RR )
102 101 adantl 
 |-  ( ( ph /\ y e. NN0 ) -> y e. RR )
103 102 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> y e. RR )
104 1red 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> 1 e. RR )
105 103 104 readdcld 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> ( y + 1 ) e. RR )
106 100 105 leloed 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> ( sum_ i e. S ( f ` i ) <_ ( y + 1 ) <-> ( sum_ i e. S ( f ` i ) < ( y + 1 ) \/ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) )
107 94 106 mpbid 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> ( sum_ i e. S ( f ` i ) < ( y + 1 ) \/ sum_ i e. S ( f ` i ) = ( y + 1 ) ) )
108 99 nn0zd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> sum_ i e. S ( f ` i ) e. ZZ )
109 nn0z 
 |-  ( y e. NN0 -> y e. ZZ )
110 109 adantl 
 |-  ( ( ph /\ y e. NN0 ) -> y e. ZZ )
111 110 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> y e. ZZ )
112 zleltp1 
 |-  ( ( sum_ i e. S ( f ` i ) e. ZZ /\ y e. ZZ ) -> ( sum_ i e. S ( f ` i ) <_ y <-> sum_ i e. S ( f ` i ) < ( y + 1 ) ) )
113 112 bicomd 
 |-  ( ( sum_ i e. S ( f ` i ) e. ZZ /\ y e. ZZ ) -> ( sum_ i e. S ( f ` i ) < ( y + 1 ) <-> sum_ i e. S ( f ` i ) <_ y ) )
114 108 111 113 syl2anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> ( sum_ i e. S ( f ` i ) < ( y + 1 ) <-> sum_ i e. S ( f ` i ) <_ y ) )
115 114 orbi1d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> ( ( sum_ i e. S ( f ` i ) < ( y + 1 ) \/ sum_ i e. S ( f ` i ) = ( y + 1 ) ) <-> ( sum_ i e. S ( f ` i ) <_ y \/ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) )
116 107 115 mpbid 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> ( sum_ i e. S ( f ` i ) <_ y \/ sum_ i e. S ( f ` i ) = ( y + 1 ) ) )
117 93 116 jca 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> ( f : S --> NN0 /\ ( sum_ i e. S ( f ` i ) <_ y \/ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) )
118 andi 
 |-  ( ( f : S --> NN0 /\ ( sum_ i e. S ( f ` i ) <_ y \/ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) <-> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) \/ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) )
119 118 bicomi 
 |-  ( ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) \/ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) <-> ( f : S --> NN0 /\ ( sum_ i e. S ( f ` i ) <_ y \/ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) )
120 117 119 sylibr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) \/ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) )
121 120 ex 
 |-  ( ( ph /\ y e. NN0 ) -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) \/ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) ) )
122 simprl 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> f : S --> NN0 )
123 122 98 syldan 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> sum_ i e. S ( f ` i ) e. NN0 )
124 123 nn0red 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> sum_ i e. S ( f ` i ) e. RR )
125 102 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> y e. RR )
126 1red 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> 1 e. RR )
127 125 126 readdcld 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> ( y + 1 ) e. RR )
128 simprr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> sum_ i e. S ( f ` i ) <_ y )
129 125 lep1d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> y <_ ( y + 1 ) )
130 124 125 127 128 129 letrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> sum_ i e. S ( f ` i ) <_ ( y + 1 ) )
131 122 130 jca 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) )
132 131 ex 
 |-  ( ( ph /\ y e. NN0 ) -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) -> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) )
133 simprl 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> f : S --> NN0 )
134 simprr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> sum_ i e. S ( f ` i ) = ( y + 1 ) )
135 102 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> y e. RR )
136 1red 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> 1 e. RR )
137 135 136 readdcld 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> ( y + 1 ) e. RR )
138 137 leidd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> ( y + 1 ) <_ ( y + 1 ) )
139 134 138 eqbrtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> sum_ i e. S ( f ` i ) <_ ( y + 1 ) )
140 133 139 jca 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) )
141 140 ex 
 |-  ( ( ph /\ y e. NN0 ) -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) -> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) )
142 132 141 jaod 
 |-  ( ( ph /\ y e. NN0 ) -> ( ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) \/ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) ) )
143 121 142 impbid 
 |-  ( ( ph /\ y e. NN0 ) -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) <-> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) \/ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) ) )
144 143 abbidv 
 |-  ( ( ph /\ y e. NN0 ) -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) } = { f | ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) \/ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) } )
145 unab 
 |-  ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } u. { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) = { f | ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) \/ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) }
146 145 a1i 
 |-  ( ( ph /\ y e. NN0 ) -> ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } u. { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) = { f | ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) \/ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) } )
147 146 eqcomd 
 |-  ( ( ph /\ y e. NN0 ) -> { f | ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) \/ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) } = ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } u. { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) )
148 144 147 eqtrd 
 |-  ( ( ph /\ y e. NN0 ) -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) } = ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } u. { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) )
149 148 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) } = ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } u. { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) )
150 149 fveq2d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) } ) = ( # ` ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } u. { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) ) )
151 2 adantr 
 |-  ( ( ph /\ y e. NN0 ) -> S e. Fin )
152 fzfid 
 |-  ( ( ph /\ y e. NN0 ) -> ( 0 ... y ) e. Fin )
153 151 152 jca 
 |-  ( ( ph /\ y e. NN0 ) -> ( S e. Fin /\ ( 0 ... y ) e. Fin ) )
154 xpfi 
 |-  ( ( S e. Fin /\ ( 0 ... y ) e. Fin ) -> ( S X. ( 0 ... y ) ) e. Fin )
155 153 154 syl 
 |-  ( ( ph /\ y e. NN0 ) -> ( S X. ( 0 ... y ) ) e. Fin )
156 pwfi 
 |-  ( ( S X. ( 0 ... y ) ) e. Fin <-> ~P ( S X. ( 0 ... y ) ) e. Fin )
157 155 156 sylib 
 |-  ( ( ph /\ y e. NN0 ) -> ~P ( S X. ( 0 ... y ) ) e. Fin )
158 fsetsspwxp 
 |-  { f | f : S --> ( 0 ... y ) } C_ ~P ( S X. ( 0 ... y ) )
159 158 a1i 
 |-  ( ( ph /\ y e. NN0 ) -> { f | f : S --> ( 0 ... y ) } C_ ~P ( S X. ( 0 ... y ) ) )
160 157 159 ssfid 
 |-  ( ( ph /\ y e. NN0 ) -> { f | f : S --> ( 0 ... y ) } e. Fin )
161 ffn 
 |-  ( f : S --> NN0 -> f Fn S )
162 122 161 syl 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> f Fn S )
163 0zd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> 0 e. ZZ )
164 110 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> y e. ZZ )
165 164 adantr 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> y e. ZZ )
166 122 ffvelcdmda 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( f ` s ) e. NN0 )
167 166 nn0zd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( f ` s ) e. ZZ )
168 166 nn0ge0d 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> 0 <_ ( f ` s ) )
169 128 ad2antrr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) /\ y < ( f ` s ) ) -> sum_ i e. S ( f ` i ) <_ y )
170 125 ad2antrr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) /\ y < ( f ` s ) ) -> y e. RR )
171 166 nn0red 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( f ` s ) e. RR )
172 171 adantr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) /\ y < ( f ` s ) ) -> ( f ` s ) e. RR )
173 124 adantr 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> sum_ i e. S ( f ` i ) e. RR )
174 173 adantr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) /\ y < ( f ` s ) ) -> sum_ i e. S ( f ` i ) e. RR )
175 simpr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) /\ y < ( f ` s ) ) -> y < ( f ` s ) )
176 simplll 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ph )
177 simpllr 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> y e. NN0 )
178 simplrl 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> f : S --> NN0 )
179 176 177 178 jca31 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) )
180 difssd 
 |-  ( ph -> ( S \ { s } ) C_ S )
181 2 180 ssfid 
 |-  ( ph -> ( S \ { s } ) e. Fin )
182 181 adantr 
 |-  ( ( ph /\ y e. NN0 ) -> ( S \ { s } ) e. Fin )
183 182 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) -> ( S \ { s } ) e. Fin )
184 eldifi 
 |-  ( i e. ( S \ { s } ) -> i e. S )
185 184 adantl 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) /\ i e. ( S \ { s } ) ) -> i e. S )
186 97 adantlr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) /\ i e. ( S \ { s } ) ) /\ i e. S ) -> ( f ` i ) e. NN0 )
187 185 186 mpdan 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) /\ i e. ( S \ { s } ) ) -> ( f ` i ) e. NN0 )
188 183 187 fsumnn0cl 
 |-  ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) -> sum_ i e. ( S \ { s } ) ( f ` i ) e. NN0 )
189 179 188 syl 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> sum_ i e. ( S \ { s } ) ( f ` i ) e. NN0 )
190 189 nn0ge0d 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> 0 <_ sum_ i e. ( S \ { s } ) ( f ` i ) )
191 difssd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) -> ( S \ { s } ) C_ S )
192 95 191 ssfid 
 |-  ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) -> ( S \ { s } ) e. Fin )
193 192 187 fsumnn0cl 
 |-  ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) -> sum_ i e. ( S \ { s } ) ( f ` i ) e. NN0 )
194 179 193 syl 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> sum_ i e. ( S \ { s } ) ( f ` i ) e. NN0 )
195 194 nn0red 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> sum_ i e. ( S \ { s } ) ( f ` i ) e. RR )
196 171 195 addge01d 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( 0 <_ sum_ i e. ( S \ { s } ) ( f ` i ) <-> ( f ` s ) <_ ( ( f ` s ) + sum_ i e. ( S \ { s } ) ( f ` i ) ) ) )
197 190 196 mpbid 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( f ` s ) <_ ( ( f ` s ) + sum_ i e. ( S \ { s } ) ( f ` i ) ) )
198 simpr 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> s e. S )
199 179 198 jca 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) /\ s e. S ) )
200 nfv 
 |-  F/ i ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) /\ s e. S )
201 nfcv 
 |-  F/_ i ( f ` s )
202 95 adantr 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) /\ s e. S ) -> S e. Fin )
203 97 adantlr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) /\ s e. S ) /\ i e. S ) -> ( f ` i ) e. NN0 )
204 203 nn0cnd 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) /\ s e. S ) /\ i e. S ) -> ( f ` i ) e. CC )
205 simpr 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) /\ s e. S ) -> s e. S )
206 fveq2 
 |-  ( i = s -> ( f ` i ) = ( f ` s ) )
207 200 201 202 204 205 206 fsumsplit1 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ f : S --> NN0 ) /\ s e. S ) -> sum_ i e. S ( f ` i ) = ( ( f ` s ) + sum_ i e. ( S \ { s } ) ( f ` i ) ) )
208 199 207 syl 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> sum_ i e. S ( f ` i ) = ( ( f ` s ) + sum_ i e. ( S \ { s } ) ( f ` i ) ) )
209 208 eqcomd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( ( f ` s ) + sum_ i e. ( S \ { s } ) ( f ` i ) ) = sum_ i e. S ( f ` i ) )
210 197 209 breqtrd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( f ` s ) <_ sum_ i e. S ( f ` i ) )
211 210 adantr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) /\ y < ( f ` s ) ) -> ( f ` s ) <_ sum_ i e. S ( f ` i ) )
212 170 172 174 175 211 ltletrd 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) /\ y < ( f ` s ) ) -> y < sum_ i e. S ( f ` i ) )
213 170 174 ltnled 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) /\ y < ( f ` s ) ) -> ( y < sum_ i e. S ( f ` i ) <-> -. sum_ i e. S ( f ` i ) <_ y ) )
214 212 213 mpbid 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) /\ y < ( f ` s ) ) -> -. sum_ i e. S ( f ` i ) <_ y )
215 169 214 pm2.21dd 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) /\ y < ( f ` s ) ) -> -. y < ( f ` s ) )
216 215 pm2.01da 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> -. y < ( f ` s ) )
217 177 101 syl 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> y e. RR )
218 171 217 lenltd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( ( f ` s ) <_ y <-> -. y < ( f ` s ) ) )
219 216 218 mpbird 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( f ` s ) <_ y )
220 163 165 167 168 219 elfzd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) /\ s e. S ) -> ( f ` s ) e. ( 0 ... y ) )
221 220 ralrimiva 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> A. s e. S ( f ` s ) e. ( 0 ... y ) )
222 162 221 jca 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> ( f Fn S /\ A. s e. S ( f ` s ) e. ( 0 ... y ) ) )
223 ffnfv 
 |-  ( f : S --> ( 0 ... y ) <-> ( f Fn S /\ A. s e. S ( f ` s ) e. ( 0 ... y ) ) )
224 222 223 sylibr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> f : S --> ( 0 ... y ) )
225 224 ex 
 |-  ( ( ph /\ y e. NN0 ) -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) -> f : S --> ( 0 ... y ) ) )
226 225 ss2abdv 
 |-  ( ( ph /\ y e. NN0 ) -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } C_ { f | f : S --> ( 0 ... y ) } )
227 160 226 ssfid 
 |-  ( ( ph /\ y e. NN0 ) -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } e. Fin )
228 227 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } e. Fin )
229 fzfid 
 |-  ( ( ph /\ y e. NN0 ) -> ( 0 ... ( y + 1 ) ) e. Fin )
230 151 229 jca 
 |-  ( ( ph /\ y e. NN0 ) -> ( S e. Fin /\ ( 0 ... ( y + 1 ) ) e. Fin ) )
231 xpfi 
 |-  ( ( S e. Fin /\ ( 0 ... ( y + 1 ) ) e. Fin ) -> ( S X. ( 0 ... ( y + 1 ) ) ) e. Fin )
232 230 231 syl 
 |-  ( ( ph /\ y e. NN0 ) -> ( S X. ( 0 ... ( y + 1 ) ) ) e. Fin )
233 pwfi 
 |-  ( ( S X. ( 0 ... ( y + 1 ) ) ) e. Fin <-> ~P ( S X. ( 0 ... ( y + 1 ) ) ) e. Fin )
234 232 233 sylib 
 |-  ( ( ph /\ y e. NN0 ) -> ~P ( S X. ( 0 ... ( y + 1 ) ) ) e. Fin )
235 fsetsspwxp 
 |-  { f | f : S --> ( 0 ... ( y + 1 ) ) } C_ ~P ( S X. ( 0 ... ( y + 1 ) ) )
236 235 a1i 
 |-  ( ( ph /\ y e. NN0 ) -> { f | f : S --> ( 0 ... ( y + 1 ) ) } C_ ~P ( S X. ( 0 ... ( y + 1 ) ) ) )
237 234 236 ssfid 
 |-  ( ( ph /\ y e. NN0 ) -> { f | f : S --> ( 0 ... ( y + 1 ) ) } e. Fin )
238 161 ad2antrl 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> f Fn S )
239 0zd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> 0 e. ZZ )
240 simpllr 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> y e. NN0 )
241 240 nn0zd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> y e. ZZ )
242 241 peano2zd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> ( y + 1 ) e. ZZ )
243 133 ffvelcdmda 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> ( f ` s ) e. NN0 )
244 243 nn0zd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> ( f ` s ) e. ZZ )
245 243 nn0ge0d 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> 0 <_ ( f ` s ) )
246 134 ad2antrr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> sum_ i e. S ( f ` i ) = ( y + 1 ) )
247 137 ad2antrr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> ( y + 1 ) e. RR )
248 133 ad2antrr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> f : S --> NN0 )
249 simplr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> s e. S )
250 248 249 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> ( f ` s ) e. NN0 )
251 250 nn0red 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> ( f ` s ) e. RR )
252 246 247 eqeltrd 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> sum_ i e. S ( f ` i ) e. RR )
253 simpr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> ( y + 1 ) < ( f ` s ) )
254 133 188 syldan 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> sum_ i e. ( S \ { s } ) ( f ` i ) e. NN0 )
255 254 adantr 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> sum_ i e. ( S \ { s } ) ( f ` i ) e. NN0 )
256 255 adantr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> sum_ i e. ( S \ { s } ) ( f ` i ) e. NN0 )
257 256 nn0ge0d 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> 0 <_ sum_ i e. ( S \ { s } ) ( f ` i ) )
258 256 nn0red 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> sum_ i e. ( S \ { s } ) ( f ` i ) e. RR )
259 251 258 addge01d 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> ( 0 <_ sum_ i e. ( S \ { s } ) ( f ` i ) <-> ( f ` s ) <_ ( ( f ` s ) + sum_ i e. ( S \ { s } ) ( f ` i ) ) ) )
260 257 259 mpbid 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> ( f ` s ) <_ ( ( f ` s ) + sum_ i e. ( S \ { s } ) ( f ` i ) ) )
261 133 207 syldanl 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> sum_ i e. S ( f ` i ) = ( ( f ` s ) + sum_ i e. ( S \ { s } ) ( f ` i ) ) )
262 261 adantr 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> sum_ i e. S ( f ` i ) = ( ( f ` s ) + sum_ i e. ( S \ { s } ) ( f ` i ) ) )
263 262 eqcomd 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> ( ( f ` s ) + sum_ i e. ( S \ { s } ) ( f ` i ) ) = sum_ i e. S ( f ` i ) )
264 260 263 breqtrd 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> ( f ` s ) <_ sum_ i e. S ( f ` i ) )
265 247 251 252 253 264 ltletrd 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> ( y + 1 ) < sum_ i e. S ( f ` i ) )
266 247 265 ltned 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> ( y + 1 ) =/= sum_ i e. S ( f ` i ) )
267 266 necomd 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> sum_ i e. S ( f ` i ) =/= ( y + 1 ) )
268 246 267 pm2.21ddne 
 |-  ( ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) /\ ( y + 1 ) < ( f ` s ) ) -> -. ( y + 1 ) < ( f ` s ) )
269 268 pm2.01da 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> -. ( y + 1 ) < ( f ` s ) )
270 243 nn0red 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> ( f ` s ) e. RR )
271 137 adantr 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> ( y + 1 ) e. RR )
272 270 271 lenltd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> ( ( f ` s ) <_ ( y + 1 ) <-> -. ( y + 1 ) < ( f ` s ) ) )
273 269 272 mpbird 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> ( f ` s ) <_ ( y + 1 ) )
274 239 242 244 245 273 elfzd 
 |-  ( ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) /\ s e. S ) -> ( f ` s ) e. ( 0 ... ( y + 1 ) ) )
275 274 ralrimiva 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> A. s e. S ( f ` s ) e. ( 0 ... ( y + 1 ) ) )
276 238 275 jca 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> ( f Fn S /\ A. s e. S ( f ` s ) e. ( 0 ... ( y + 1 ) ) ) )
277 ffnfv 
 |-  ( f : S --> ( 0 ... ( y + 1 ) ) <-> ( f Fn S /\ A. s e. S ( f ` s ) e. ( 0 ... ( y + 1 ) ) ) )
278 276 277 sylibr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) -> f : S --> ( 0 ... ( y + 1 ) ) )
279 278 ex 
 |-  ( ( ph /\ y e. NN0 ) -> ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) -> f : S --> ( 0 ... ( y + 1 ) ) ) )
280 279 ss2abdv 
 |-  ( ( ph /\ y e. NN0 ) -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } C_ { f | f : S --> ( 0 ... ( y + 1 ) ) } )
281 237 280 ssfid 
 |-  ( ( ph /\ y e. NN0 ) -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } e. Fin )
282 281 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } e. Fin )
283 inab 
 |-  ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } i^i { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) = { f | ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) }
284 283 a1i 
 |-  ( ( ph /\ y e. NN0 ) -> ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } i^i { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) = { f | ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) } )
285 98 adantrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> sum_ i e. S ( f ` i ) e. NN0 )
286 285 nn0zd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> sum_ i e. S ( f ` i ) e. ZZ )
287 286 zred 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> sum_ i e. S ( f ` i ) e. RR )
288 125 ltp1d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> y < ( y + 1 ) )
289 287 125 127 128 288 lelttrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> sum_ i e. S ( f ` i ) < ( y + 1 ) )
290 287 289 ltned 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> sum_ i e. S ( f ` i ) =/= ( y + 1 ) )
291 290 neneqd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> -. sum_ i e. S ( f ` i ) = ( y + 1 ) )
292 291 intnand 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> -. ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) )
293 nan 
 |-  ( ( ( ph /\ y e. NN0 ) -> -. ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) ) <-> ( ( ( ph /\ y e. NN0 ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) ) -> -. ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) )
294 292 293 mpbir 
 |-  ( ( ph /\ y e. NN0 ) -> -. ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) )
295 294 alrimiv 
 |-  ( ( ph /\ y e. NN0 ) -> A. f -. ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) )
296 ab0 
 |-  ( { f | ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) } = (/) <-> A. f -. ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) )
297 295 296 sylibr 
 |-  ( ( ph /\ y e. NN0 ) -> { f | ( ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) /\ ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) ) } = (/) )
298 284 297 eqtrd 
 |-  ( ( ph /\ y e. NN0 ) -> ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } i^i { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) = (/) )
299 298 adantr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } i^i { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) = (/) )
300 hashun 
 |-  ( ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } e. Fin /\ { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } e. Fin /\ ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } i^i { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) = (/) ) -> ( # ` ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } u. { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) ) = ( ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) + ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) ) )
301 228 282 299 300 syl3anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( # ` ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } u. { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) ) = ( ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) + ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) ) )
302 simpr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) )
303 simplr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> y e. NN0 )
304 1nn0 
 |-  1 e. NN0
305 304 a1i 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> 1 e. NN0 )
306 303 305 nn0addcld 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( y + 1 ) e. NN0 )
307 2 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> S e. Fin )
308 3 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> S =/= (/) )
309 eqid 
 |-  { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } = { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) }
310 306 307 308 309 sticksstones21 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) = ( ( ( y + 1 ) + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) )
311 302 310 oveq12d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) + ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) ) = ( ( ( y + ( # ` S ) ) _C ( # ` S ) ) + ( ( ( y + 1 ) + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) ) )
312 303 nn0cnd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> y e. CC )
313 1cnd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> 1 e. CC )
314 71 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( # ` S ) e. CC )
315 312 313 314 ppncand 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( ( y + 1 ) + ( ( # ` S ) - 1 ) ) = ( y + ( # ` S ) ) )
316 315 oveq1d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( ( ( y + 1 ) + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) = ( ( y + ( # ` S ) ) _C ( ( # ` S ) - 1 ) ) )
317 316 oveq2d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( ( ( y + ( # ` S ) ) _C ( # ` S ) ) + ( ( ( y + 1 ) + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) ) = ( ( ( y + ( # ` S ) ) _C ( # ` S ) ) + ( ( y + ( # ` S ) ) _C ( ( # ` S ) - 1 ) ) ) )
318 82 ad2antrr 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( # ` S ) e. NN0 )
319 303 318 nn0addcld 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( y + ( # ` S ) ) e. NN0 )
320 318 nn0zd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( # ` S ) e. ZZ )
321 bcpasc 
 |-  ( ( ( y + ( # ` S ) ) e. NN0 /\ ( # ` S ) e. ZZ ) -> ( ( ( y + ( # ` S ) ) _C ( # ` S ) ) + ( ( y + ( # ` S ) ) _C ( ( # ` S ) - 1 ) ) ) = ( ( ( y + ( # ` S ) ) + 1 ) _C ( # ` S ) ) )
322 319 320 321 syl2anc 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( ( ( y + ( # ` S ) ) _C ( # ` S ) ) + ( ( y + ( # ` S ) ) _C ( ( # ` S ) - 1 ) ) ) = ( ( ( y + ( # ` S ) ) + 1 ) _C ( # ` S ) ) )
323 317 322 eqtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( ( ( y + ( # ` S ) ) _C ( # ` S ) ) + ( ( ( y + 1 ) + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) ) = ( ( ( y + ( # ` S ) ) + 1 ) _C ( # ` S ) ) )
324 312 314 313 add32d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( ( y + ( # ` S ) ) + 1 ) = ( ( y + 1 ) + ( # ` S ) ) )
325 324 oveq1d 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( ( ( y + ( # ` S ) ) + 1 ) _C ( # ` S ) ) = ( ( ( y + 1 ) + ( # ` S ) ) _C ( # ` S ) ) )
326 323 325 eqtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( ( ( y + ( # ` S ) ) _C ( # ` S ) ) + ( ( ( y + 1 ) + ( ( # ` S ) - 1 ) ) _C ( ( # ` S ) - 1 ) ) ) = ( ( ( y + 1 ) + ( # ` S ) ) _C ( # ` S ) ) )
327 311 326 eqtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) + ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) ) = ( ( ( y + 1 ) + ( # ` S ) ) _C ( # ` S ) ) )
328 301 327 eqtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( # ` ( { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } u. { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) = ( y + 1 ) ) } ) ) = ( ( ( y + 1 ) + ( # ` S ) ) _C ( # ` S ) ) )
329 150 328 eqtrd 
 |-  ( ( ( ph /\ y e. NN0 ) /\ ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ y ) } ) = ( ( y + ( # ` S ) ) _C ( # ` S ) ) ) -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ ( y + 1 ) ) } ) = ( ( ( y + 1 ) + ( # ` S ) ) _C ( # ` S ) ) )
330 13 20 27 34 92 329 nn0indd 
 |-  ( ( ph /\ N e. NN0 ) -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } ) = ( ( N + ( # ` S ) ) _C ( # ` S ) ) )
331 1 330 mpdan 
 |-  ( ph -> ( # ` { f | ( f : S --> NN0 /\ sum_ i e. S ( f ` i ) <_ N ) } ) = ( ( N + ( # ` S ) ) _C ( # ` S ) ) )
332 6 331 eqtrd 
 |-  ( ph -> ( # ` A ) = ( ( N + ( # ` S ) ) _C ( # ` S ) ) )