Metamath Proof Explorer

Theorem sticksstones22

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

Ref Expression
Hypotheses sticksstones22.1 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
sticksstones22.2 ⊢ ( 𝜑 → 𝑆 ∈ Fin )
sticksstones22.3 ⊢ ( 𝜑 → 𝑆 ≠ ∅ )
sticksstones22.4 ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : 𝑆 ⟶ ℕ0 ∧ Σ 𝑖 ∈ 𝑆 ( 𝑓 ‘ 𝑖 ) ≤ 𝑁 ) }
Assertion sticksstones22 ( 𝜑 → ( ♯ ‘ 𝐴 ) = ( ( 𝑁 + ( ♯ ‘ 𝑆 ) ) C ( ♯ ‘ 𝑆 ) ) )

Proof

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