Users' Mathboxes Mathbox for metakunt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  sticksstones22 Structured version   Visualization version   GIF version

Theorem sticksstones22 40576
Description: Non-exhaustive sticks and stones. (Contributed by metakunt, 26-Oct-2024.)
Hypotheses
Ref Expression
sticksstones22.1 (𝜑𝑁 ∈ ℕ0)
sticksstones22.2 (𝜑𝑆 ∈ Fin)
sticksstones22.3 (𝜑𝑆 ≠ ∅)
sticksstones22.4 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁)}
Assertion
Ref Expression
sticksstones22 (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
Distinct variable groups:   𝑓,𝑁   𝑆,𝑓,𝑖   𝜑,𝑓,𝑖
Allowed substitution hints:   𝐴(𝑓,𝑖)   𝑁(𝑖)

Proof of Theorem sticksstones22
Dummy variables 𝑥 𝑠 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sticksstones22.4 . . . 4 𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁)}
21a1i 11 . . 3 (𝜑𝐴 = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁)})
32fveq2d 6846 . 2 (𝜑 → (♯‘𝐴) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁)}))
4 sticksstones22.1 . . 3 (𝜑𝑁 ∈ ℕ0)
5 breq2 5109 . . . . . . . 8 (𝑥 = 0 → (Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥 ↔ Σ𝑖𝑆 (𝑓𝑖) ≤ 0))
65anbi2d 629 . . . . . . 7 (𝑥 = 0 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)))
76abbidv 2805 . . . . . 6 (𝑥 = 0 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)})
87fveq2d 6846 . . . . 5 (𝑥 = 0 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)}))
9 oveq1 7364 . . . . . 6 (𝑥 = 0 → (𝑥 + (♯‘𝑆)) = (0 + (♯‘𝑆)))
109oveq1d 7372 . . . . 5 (𝑥 = 0 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
118, 10eqeq12d 2752 . . . 4 (𝑥 = 0 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆))))
12 breq2 5109 . . . . . . . 8 (𝑥 = 𝑦 → (Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥 ↔ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦))
1312anbi2d 629 . . . . . . 7 (𝑥 = 𝑦 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)))
1413abbidv 2805 . . . . . 6 (𝑥 = 𝑦 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)})
1514fveq2d 6846 . . . . 5 (𝑥 = 𝑦 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}))
16 oveq1 7364 . . . . . 6 (𝑥 = 𝑦 → (𝑥 + (♯‘𝑆)) = (𝑦 + (♯‘𝑆)))
1716oveq1d 7372 . . . . 5 (𝑥 = 𝑦 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆)))
1815, 17eqeq12d 2752 . . . 4 (𝑥 = 𝑦 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))))
19 breq2 5109 . . . . . . . 8 (𝑥 = (𝑦 + 1) → (Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥 ↔ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1)))
2019anbi2d 629 . . . . . . 7 (𝑥 = (𝑦 + 1) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))))
2120abbidv 2805 . . . . . 6 (𝑥 = (𝑦 + 1) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))})
2221fveq2d 6846 . . . . 5 (𝑥 = (𝑦 + 1) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))}))
23 oveq1 7364 . . . . . 6 (𝑥 = (𝑦 + 1) → (𝑥 + (♯‘𝑆)) = ((𝑦 + 1) + (♯‘𝑆)))
2423oveq1d 7372 . . . . 5 (𝑥 = (𝑦 + 1) → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
2522, 24eqeq12d 2752 . . . 4 (𝑥 = (𝑦 + 1) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))}) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆))))
26 breq2 5109 . . . . . . . 8 (𝑥 = 𝑁 → (Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥 ↔ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁))
2726anbi2d 629 . . . . . . 7 (𝑥 = 𝑁 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁)))
2827abbidv 2805 . . . . . 6 (𝑥 = 𝑁 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁)})
2928fveq2d 6846 . . . . 5 (𝑥 = 𝑁 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁)}))
30 oveq1 7364 . . . . . 6 (𝑥 = 𝑁 → (𝑥 + (♯‘𝑆)) = (𝑁 + (♯‘𝑆)))
3130oveq1d 7372 . . . . 5 (𝑥 = 𝑁 → ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
3229, 31eqeq12d 2752 . . . 4 (𝑥 = 𝑁 → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑥)}) = ((𝑥 + (♯‘𝑆))C(♯‘𝑆)) ↔ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆))))
33 simprl 769 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → 𝑓:𝑆⟶ℕ0)
34 simprr 771 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → Σ𝑖𝑆 (𝑓𝑖) ≤ 0)
35 sticksstones22.2 . . . . . . . . . . . . . . . . 17 (𝜑𝑆 ∈ Fin)
3635adantr 481 . . . . . . . . . . . . . . . 16 ((𝜑𝑓:𝑆⟶ℕ0) → 𝑆 ∈ Fin)
37 simpr 485 . . . . . . . . . . . . . . . . 17 ((𝜑𝑓:𝑆⟶ℕ0) → 𝑓:𝑆⟶ℕ0)
3837ffvelcdmda 7035 . . . . . . . . . . . . . . . 16 (((𝜑𝑓:𝑆⟶ℕ0) ∧ 𝑖𝑆) → (𝑓𝑖) ∈ ℕ0)
3936, 38fsumnn0cl 15621 . . . . . . . . . . . . . . 15 ((𝜑𝑓:𝑆⟶ℕ0) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℕ0)
4033, 39syldan 591 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℕ0)
4140nn0ge0d 12476 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → 0 ≤ Σ𝑖𝑆 (𝑓𝑖))
42 0red 11158 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → 0 ∈ ℝ)
4340nn0red 12474 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℝ)
4442, 43lenltd 11301 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → (0 ≤ Σ𝑖𝑆 (𝑓𝑖) ↔ ¬ Σ𝑖𝑆 (𝑓𝑖) < 0))
4541, 44mpbid 231 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → ¬ Σ𝑖𝑆 (𝑓𝑖) < 0)
4634, 45jca 512 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → (Σ𝑖𝑆 (𝑓𝑖) ≤ 0 ∧ ¬ Σ𝑖𝑆 (𝑓𝑖) < 0))
4743, 42eqleltd 11299 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → (Σ𝑖𝑆 (𝑓𝑖) = 0 ↔ (Σ𝑖𝑆 (𝑓𝑖) ≤ 0 ∧ ¬ Σ𝑖𝑆 (𝑓𝑖) < 0)))
4846, 47mpbird 256 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → Σ𝑖𝑆 (𝑓𝑖) = 0)
4933, 48jca 512 . . . . . . . . 9 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0))
5049ex 413 . . . . . . . 8 (𝜑 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)))
51 simprl 769 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)) → 𝑓:𝑆⟶ℕ0)
52 simprr 771 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)) → Σ𝑖𝑆 (𝑓𝑖) = 0)
53 0red 11158 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)) → 0 ∈ ℝ)
5453leidd 11721 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)) → 0 ≤ 0)
5552, 54eqbrtrd 5127 . . . . . . . . . 10 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)) → Σ𝑖𝑆 (𝑓𝑖) ≤ 0)
5651, 55jca 512 . . . . . . . . 9 ((𝜑 ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0))
5756ex 413 . . . . . . . 8 (𝜑 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)))
5850, 57impbid 211 . . . . . . 7 (𝜑 → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0) ↔ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)))
5958abbidv 2805 . . . . . 6 (𝜑 → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)})
6059fveq2d 6846 . . . . 5 (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)}) = (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)}))
61 0nn0 12428 . . . . . . . 8 0 ∈ ℕ0
6261a1i 11 . . . . . . 7 (𝜑 → 0 ∈ ℕ0)
63 sticksstones22.3 . . . . . . 7 (𝜑𝑆 ≠ ∅)
64 eqid 2736 . . . . . . 7 {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)}
6562, 35, 63, 64sticksstones21 40575 . . . . . 6 (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)}) = ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
66 hashnncl 14266 . . . . . . . . . . . . . . . 16 (𝑆 ∈ Fin → ((♯‘𝑆) ∈ ℕ ↔ 𝑆 ≠ ∅))
6735, 66syl 17 . . . . . . . . . . . . . . 15 (𝜑 → ((♯‘𝑆) ∈ ℕ ↔ 𝑆 ≠ ∅))
6867bicomd 222 . . . . . . . . . . . . . 14 (𝜑 → (𝑆 ≠ ∅ ↔ (♯‘𝑆) ∈ ℕ))
6968biimpd 228 . . . . . . . . . . . . 13 (𝜑 → (𝑆 ≠ ∅ → (♯‘𝑆) ∈ ℕ))
7063, 69mpd 15 . . . . . . . . . . . 12 (𝜑 → (♯‘𝑆) ∈ ℕ)
7170nncnd 12169 . . . . . . . . . . 11 (𝜑 → (♯‘𝑆) ∈ ℂ)
72 1cnd 11150 . . . . . . . . . . 11 (𝜑 → 1 ∈ ℂ)
7371, 72subcld 11512 . . . . . . . . . 10 (𝜑 → ((♯‘𝑆) − 1) ∈ ℂ)
7473addid2d 11356 . . . . . . . . 9 (𝜑 → (0 + ((♯‘𝑆) − 1)) = ((♯‘𝑆) − 1))
7574oveq1d 7372 . . . . . . . 8 (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)))
76 nnm1nn0 12454 . . . . . . . . . 10 ((♯‘𝑆) ∈ ℕ → ((♯‘𝑆) − 1) ∈ ℕ0)
7770, 76syl 17 . . . . . . . . 9 (𝜑 → ((♯‘𝑆) − 1) ∈ ℕ0)
78 bcnn 14212 . . . . . . . . 9 (((♯‘𝑆) − 1) ∈ ℕ0 → (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)) = 1)
7977, 78syl 17 . . . . . . . 8 (𝜑 → (((♯‘𝑆) − 1)C((♯‘𝑆) − 1)) = 1)
8075, 79eqtrd 2776 . . . . . . 7 (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = 1)
81 eqidd 2737 . . . . . . 7 (𝜑 → 1 = 1)
8270nnnn0d 12473 . . . . . . . . . 10 (𝜑 → (♯‘𝑆) ∈ ℕ0)
83 bcnn 14212 . . . . . . . . . 10 ((♯‘𝑆) ∈ ℕ0 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
8482, 83syl 17 . . . . . . . . 9 (𝜑 → ((♯‘𝑆)C(♯‘𝑆)) = 1)
8584eqcomd 2742 . . . . . . . 8 (𝜑 → 1 = ((♯‘𝑆)C(♯‘𝑆)))
8671addid2d 11356 . . . . . . . . . 10 (𝜑 → (0 + (♯‘𝑆)) = (♯‘𝑆))
8786eqcomd 2742 . . . . . . . . 9 (𝜑 → (♯‘𝑆) = (0 + (♯‘𝑆)))
8887oveq1d 7372 . . . . . . . 8 (𝜑 → ((♯‘𝑆)C(♯‘𝑆)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
8985, 88eqtrd 2776 . . . . . . 7 (𝜑 → 1 = ((0 + (♯‘𝑆))C(♯‘𝑆)))
9080, 81, 893eqtrd 2780 . . . . . 6 (𝜑 → ((0 + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
9165, 90eqtrd 2776 . . . . 5 (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
9260, 91eqtrd 2776 . . . 4 (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 0)}) = ((0 + (♯‘𝑆))C(♯‘𝑆)))
93 simprl 769 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → 𝑓:𝑆⟶ℕ0)
94 simprr 771 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))
9535ad2antrr 724 . . . . . . . . . . . . . . . . . . 19 (((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → 𝑆 ∈ Fin)
96 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → 𝑓:𝑆⟶ℕ0)
9796ffvelcdmda 7035 . . . . . . . . . . . . . . . . . . 19 ((((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖𝑆) → (𝑓𝑖) ∈ ℕ0)
9895, 97fsumnn0cl 15621 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℕ0)
9993, 98syldan 591 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℕ0)
10099nn0red 12474 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℝ)
101 nn0re 12422 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ ℕ0𝑦 ∈ ℝ)
102101adantl 482 . . . . . . . . . . . . . . . . . 18 ((𝜑𝑦 ∈ ℕ0) → 𝑦 ∈ ℝ)
103102adantr 481 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℝ)
104 1red 11156 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → 1 ∈ ℝ)
105103, 104readdcld 11184 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
106100, 105leloed 11298 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → (Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1) ↔ (Σ𝑖𝑆 (𝑓𝑖) < (𝑦 + 1) ∨ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))))
10794, 106mpbid 231 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → (Σ𝑖𝑆 (𝑓𝑖) < (𝑦 + 1) ∨ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))
10899nn0zd 12525 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℤ)
109 nn0z 12524 . . . . . . . . . . . . . . . . . 18 (𝑦 ∈ ℕ0𝑦 ∈ ℤ)
110109adantl 482 . . . . . . . . . . . . . . . . 17 ((𝜑𝑦 ∈ ℕ0) → 𝑦 ∈ ℤ)
111110adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → 𝑦 ∈ ℤ)
112 zleltp1 12554 . . . . . . . . . . . . . . . . 17 ((Σ𝑖𝑆 (𝑓𝑖) ∈ ℤ ∧ 𝑦 ∈ ℤ) → (Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦 ↔ Σ𝑖𝑆 (𝑓𝑖) < (𝑦 + 1)))
113112bicomd 222 . . . . . . . . . . . . . . . 16 ((Σ𝑖𝑆 (𝑓𝑖) ∈ ℤ ∧ 𝑦 ∈ ℤ) → (Σ𝑖𝑆 (𝑓𝑖) < (𝑦 + 1) ↔ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦))
114108, 111, 113syl2anc 584 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → (Σ𝑖𝑆 (𝑓𝑖) < (𝑦 + 1) ↔ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦))
115114orbi1d 915 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → ((Σ𝑖𝑆 (𝑓𝑖) < (𝑦 + 1) ∨ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)) ↔ (Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦 ∨ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))))
116107, 115mpbid 231 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → (Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦 ∨ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))
11793, 116jca 512 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦 ∨ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))))
118 andi 1006 . . . . . . . . . . . . 13 ((𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦 ∨ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ↔ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))))
119118bicomi 223 . . . . . . . . . . . 12 (((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ↔ (𝑓:𝑆⟶ℕ0 ∧ (Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦 ∨ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))))
120117, 119sylibr 233 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))))
121120ex 413 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1)) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))))
122 simprl 769 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → 𝑓:𝑆⟶ℕ0)
123122, 98syldan 591 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℕ0)
124123nn0red 12474 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℝ)
125102adantr 481 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → 𝑦 ∈ ℝ)
126 1red 11156 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → 1 ∈ ℝ)
127125, 126readdcld 11184 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → (𝑦 + 1) ∈ ℝ)
128 simprr 771 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)
129125lep1d 12086 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → 𝑦 ≤ (𝑦 + 1))
130124, 125, 127, 128, 129letrd 11312 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))
131122, 130jca 512 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1)))
132131ex 413 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))))
133 simprl 769 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → 𝑓:𝑆⟶ℕ0)
134 simprr 771 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))
135102adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → 𝑦 ∈ ℝ)
136 1red 11156 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → 1 ∈ ℝ)
137135, 136readdcld 11184 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → (𝑦 + 1) ∈ ℝ)
138137leidd 11721 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → (𝑦 + 1) ≤ (𝑦 + 1))
139134, 138eqbrtrd 5127 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))
140133, 139jca 512 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1)))
141140ex 413 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))))
142132, 141jaod 857 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℕ0) → (((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))))
143121, 142impbid 211 . . . . . . . . 9 ((𝜑𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1)) ↔ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))))
144143abbidv 2805 . . . . . . . 8 ((𝜑𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))} = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))})
145 unab 4258 . . . . . . . . . 10 ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))}
146145a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))})
147146eqcomd 2742 . . . . . . . 8 ((𝜑𝑦 ∈ ℕ0) → {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∨ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}))
148144, 147eqtrd 2776 . . . . . . 7 ((𝜑𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}))
149148adantr 481 . . . . . 6 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))} = ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}))
150149fveq2d 6846 . . . . 5 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))}) = (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))})))
15135adantr 481 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℕ0) → 𝑆 ∈ Fin)
152 fzfid 13878 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℕ0) → (0...𝑦) ∈ Fin)
153151, 152jca 512 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin))
154 xpfi 9261 . . . . . . . . . . . 12 ((𝑆 ∈ Fin ∧ (0...𝑦) ∈ Fin) → (𝑆 × (0...𝑦)) ∈ Fin)
155153, 154syl 17 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℕ0) → (𝑆 × (0...𝑦)) ∈ Fin)
156 pwfi 9122 . . . . . . . . . . 11 ((𝑆 × (0...𝑦)) ∈ Fin ↔ 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
157155, 156sylib 217 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...𝑦)) ∈ Fin)
158 fsetsspwxp 8791 . . . . . . . . . . 11 {𝑓𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦))
159158a1i 11 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℕ0) → {𝑓𝑓:𝑆⟶(0...𝑦)} ⊆ 𝒫 (𝑆 × (0...𝑦)))
160157, 159ssfid 9211 . . . . . . . . 9 ((𝜑𝑦 ∈ ℕ0) → {𝑓𝑓:𝑆⟶(0...𝑦)} ∈ Fin)
161 ffn 6668 . . . . . . . . . . . . . 14 (𝑓:𝑆⟶ℕ0𝑓 Fn 𝑆)
162122, 161syl 17 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → 𝑓 Fn 𝑆)
163 0zd 12511 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → 0 ∈ ℤ)
164110adantr 481 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → 𝑦 ∈ ℤ)
165164adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → 𝑦 ∈ ℤ)
166122ffvelcdmda 7035 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → (𝑓𝑠) ∈ ℕ0)
167166nn0zd 12525 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → (𝑓𝑠) ∈ ℤ)
168166nn0ge0d 12476 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → 0 ≤ (𝑓𝑠))
169128ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) ∧ 𝑦 < (𝑓𝑠)) → Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)
170125ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) ∧ 𝑦 < (𝑓𝑠)) → 𝑦 ∈ ℝ)
171166nn0red 12474 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → (𝑓𝑠) ∈ ℝ)
172171adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) ∧ 𝑦 < (𝑓𝑠)) → (𝑓𝑠) ∈ ℝ)
173124adantr 481 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℝ)
174173adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) ∧ 𝑦 < (𝑓𝑠)) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℝ)
175 simpr 485 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) ∧ 𝑦 < (𝑓𝑠)) → 𝑦 < (𝑓𝑠))
176 simplll 773 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → 𝜑)
177 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → 𝑦 ∈ ℕ0)
178 simplrl 775 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → 𝑓:𝑆⟶ℕ0)
179176, 177, 178jca31 515 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → ((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0))
180 difssd 4092 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (𝜑 → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
18135, 180ssfid 9211 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝜑 → (𝑆 ∖ {𝑠}) ∈ Fin)
182181adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝜑𝑦 ∈ ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
183182adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
184 eldifi 4086 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑖 ∈ (𝑆 ∖ {𝑠}) → 𝑖𝑆)
185184adantl 482 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) → 𝑖𝑆)
18697adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) ∧ 𝑖𝑆) → (𝑓𝑖) ∈ ℕ0)
187185, 186mpdan 685 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑖 ∈ (𝑆 ∖ {𝑠})) → (𝑓𝑖) ∈ ℕ0)
188183, 187fsumnn0cl 15621 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖) ∈ ℕ0)
189179, 188syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖) ∈ ℕ0)
190189nn0ge0d 12476 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖))
191 difssd 4092 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ⊆ 𝑆)
19295, 191ssfid 9211 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → (𝑆 ∖ {𝑠}) ∈ Fin)
193192, 187fsumnn0cl 15621 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖) ∈ ℕ0)
194179, 193syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖) ∈ ℕ0)
195194nn0red 12474 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖) ∈ ℝ)
196171, 195addge01d 11743 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → (0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖) ↔ (𝑓𝑠) ≤ ((𝑓𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖))))
197190, 196mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → (𝑓𝑠) ≤ ((𝑓𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖)))
198 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → 𝑠𝑆)
199179, 198jca 512 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → (((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠𝑆))
200 nfv 1917 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖(((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠𝑆)
201 nfcv 2907 . . . . . . . . . . . . . . . . . . . . . . . . 25 𝑖(𝑓𝑠)
20295adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠𝑆) → 𝑆 ∈ Fin)
20397adantlr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠𝑆) ∧ 𝑖𝑆) → (𝑓𝑖) ∈ ℕ0)
204203nn0cnd 12475 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠𝑆) ∧ 𝑖𝑆) → (𝑓𝑖) ∈ ℂ)
205 simpr 485 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠𝑆) → 𝑠𝑆)
206 fveq2 6842 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑖 = 𝑠 → (𝑓𝑖) = (𝑓𝑠))
207200, 201, 202, 204, 205, 206fsumsplit1 15630 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦 ∈ ℕ0) ∧ 𝑓:𝑆⟶ℕ0) ∧ 𝑠𝑆) → Σ𝑖𝑆 (𝑓𝑖) = ((𝑓𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖)))
208199, 207syl 17 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → Σ𝑖𝑆 (𝑓𝑖) = ((𝑓𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖)))
209208eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → ((𝑓𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖)) = Σ𝑖𝑆 (𝑓𝑖))
210197, 209breqtrd 5131 . . . . . . . . . . . . . . . . . . . . 21 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → (𝑓𝑠) ≤ Σ𝑖𝑆 (𝑓𝑖))
211210adantr 481 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) ∧ 𝑦 < (𝑓𝑠)) → (𝑓𝑠) ≤ Σ𝑖𝑆 (𝑓𝑖))
212170, 172, 174, 175, 211ltletrd 11315 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) ∧ 𝑦 < (𝑓𝑠)) → 𝑦 < Σ𝑖𝑆 (𝑓𝑖))
213170, 174ltnled 11302 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) ∧ 𝑦 < (𝑓𝑠)) → (𝑦 < Σ𝑖𝑆 (𝑓𝑖) ↔ ¬ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦))
214212, 213mpbid 231 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) ∧ 𝑦 < (𝑓𝑠)) → ¬ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)
215169, 214pm2.21dd 194 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) ∧ 𝑦 < (𝑓𝑠)) → ¬ 𝑦 < (𝑓𝑠))
216215pm2.01da 797 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → ¬ 𝑦 < (𝑓𝑠))
217177, 101syl 17 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → 𝑦 ∈ ℝ)
218171, 217lenltd 11301 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → ((𝑓𝑠) ≤ 𝑦 ↔ ¬ 𝑦 < (𝑓𝑠)))
219216, 218mpbird 256 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → (𝑓𝑠) ≤ 𝑦)
220163, 165, 167, 168, 219elfzd 13432 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) ∧ 𝑠𝑆) → (𝑓𝑠) ∈ (0...𝑦))
221220ralrimiva 3143 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → ∀𝑠𝑆 (𝑓𝑠) ∈ (0...𝑦))
222162, 221jca 512 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → (𝑓 Fn 𝑆 ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ (0...𝑦)))
223 ffnfv 7066 . . . . . . . . . . . 12 (𝑓:𝑆⟶(0...𝑦) ↔ (𝑓 Fn 𝑆 ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ (0...𝑦)))
224222, 223sylibr 233 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → 𝑓:𝑆⟶(0...𝑦))
225224ex 413 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) → 𝑓:𝑆⟶(0...𝑦)))
226225ss2abdv 4020 . . . . . . . . 9 ((𝜑𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ⊆ {𝑓𝑓:𝑆⟶(0...𝑦)})
227160, 226ssfid 9211 . . . . . . . 8 ((𝜑𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∈ Fin)
228227adantr 481 . . . . . . 7 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∈ Fin)
229 fzfid 13878 . . . . . . . . . . . . 13 ((𝜑𝑦 ∈ ℕ0) → (0...(𝑦 + 1)) ∈ Fin)
230151, 229jca 512 . . . . . . . . . . . 12 ((𝜑𝑦 ∈ ℕ0) → (𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin))
231 xpfi 9261 . . . . . . . . . . . 12 ((𝑆 ∈ Fin ∧ (0...(𝑦 + 1)) ∈ Fin) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
232230, 231syl 17 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℕ0) → (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
233 pwfi 9122 . . . . . . . . . . 11 ((𝑆 × (0...(𝑦 + 1))) ∈ Fin ↔ 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
234232, 233sylib 217 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℕ0) → 𝒫 (𝑆 × (0...(𝑦 + 1))) ∈ Fin)
235 fsetsspwxp 8791 . . . . . . . . . . 11 {𝑓𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1)))
236235a1i 11 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℕ0) → {𝑓𝑓:𝑆⟶(0...(𝑦 + 1))} ⊆ 𝒫 (𝑆 × (0...(𝑦 + 1))))
237234, 236ssfid 9211 . . . . . . . . 9 ((𝜑𝑦 ∈ ℕ0) → {𝑓𝑓:𝑆⟶(0...(𝑦 + 1))} ∈ Fin)
238161ad2antrl 726 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → 𝑓 Fn 𝑆)
239 0zd 12511 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → 0 ∈ ℤ)
240 simpllr 774 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → 𝑦 ∈ ℕ0)
241240nn0zd 12525 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → 𝑦 ∈ ℤ)
242241peano2zd 12610 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → (𝑦 + 1) ∈ ℤ)
243133ffvelcdmda 7035 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → (𝑓𝑠) ∈ ℕ0)
244243nn0zd 12525 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → (𝑓𝑠) ∈ ℤ)
245243nn0ge0d 12476 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → 0 ≤ (𝑓𝑠))
246134ad2antrr 724 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))
247137ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → (𝑦 + 1) ∈ ℝ)
248133ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → 𝑓:𝑆⟶ℕ0)
249 simplr 767 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → 𝑠𝑆)
250248, 249ffvelcdmd 7036 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → (𝑓𝑠) ∈ ℕ0)
251250nn0red 12474 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → (𝑓𝑠) ∈ ℝ)
252246, 247eqeltrd 2838 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℝ)
253 simpr 485 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → (𝑦 + 1) < (𝑓𝑠))
254133, 188syldan 591 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖) ∈ ℕ0)
255254adantr 481 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖) ∈ ℕ0)
256255adantr 481 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖) ∈ ℕ0)
257256nn0ge0d 12476 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → 0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖))
258256nn0red 12474 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖) ∈ ℝ)
259251, 258addge01d 11743 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → (0 ≤ Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖) ↔ (𝑓𝑠) ≤ ((𝑓𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖))))
260257, 259mpbid 231 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → (𝑓𝑠) ≤ ((𝑓𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖)))
261133, 207syldanl 602 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → Σ𝑖𝑆 (𝑓𝑖) = ((𝑓𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖)))
262261adantr 481 . . . . . . . . . . . . . . . . . . . . . . 23 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → Σ𝑖𝑆 (𝑓𝑖) = ((𝑓𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖)))
263262eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . 22 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → ((𝑓𝑠) + Σ𝑖 ∈ (𝑆 ∖ {𝑠})(𝑓𝑖)) = Σ𝑖𝑆 (𝑓𝑖))
264260, 263breqtrd 5131 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → (𝑓𝑠) ≤ Σ𝑖𝑆 (𝑓𝑖))
265247, 251, 252, 253, 264ltletrd 11315 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → (𝑦 + 1) < Σ𝑖𝑆 (𝑓𝑖))
266247, 265ltned 11291 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → (𝑦 + 1) ≠ Σ𝑖𝑆 (𝑓𝑖))
267266necomd 2999 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → Σ𝑖𝑆 (𝑓𝑖) ≠ (𝑦 + 1))
268246, 267pm2.21ddne 3029 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) ∧ (𝑦 + 1) < (𝑓𝑠)) → ¬ (𝑦 + 1) < (𝑓𝑠))
269268pm2.01da 797 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → ¬ (𝑦 + 1) < (𝑓𝑠))
270243nn0red 12474 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → (𝑓𝑠) ∈ ℝ)
271137adantr 481 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → (𝑦 + 1) ∈ ℝ)
272270, 271lenltd 11301 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → ((𝑓𝑠) ≤ (𝑦 + 1) ↔ ¬ (𝑦 + 1) < (𝑓𝑠)))
273269, 272mpbird 256 . . . . . . . . . . . . . . 15 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → (𝑓𝑠) ≤ (𝑦 + 1))
274239, 242, 244, 245, 273elfzd 13432 . . . . . . . . . . . . . 14 ((((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) ∧ 𝑠𝑆) → (𝑓𝑠) ∈ (0...(𝑦 + 1)))
275274ralrimiva 3143 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → ∀𝑠𝑆 (𝑓𝑠) ∈ (0...(𝑦 + 1)))
276238, 275jca 512 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → (𝑓 Fn 𝑆 ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ (0...(𝑦 + 1))))
277 ffnfv 7066 . . . . . . . . . . . 12 (𝑓:𝑆⟶(0...(𝑦 + 1)) ↔ (𝑓 Fn 𝑆 ∧ ∀𝑠𝑆 (𝑓𝑠) ∈ (0...(𝑦 + 1))))
278276, 277sylibr 233 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))) → 𝑓:𝑆⟶(0...(𝑦 + 1)))
279278ex 413 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℕ0) → ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)) → 𝑓:𝑆⟶(0...(𝑦 + 1))))
280279ss2abdv 4020 . . . . . . . . 9 ((𝜑𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))} ⊆ {𝑓𝑓:𝑆⟶(0...(𝑦 + 1))})
281237, 280ssfid 9211 . . . . . . . 8 ((𝜑𝑦 ∈ ℕ0) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))} ∈ Fin)
282281adantr 481 . . . . . . 7 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))} ∈ Fin)
283 inab 4259 . . . . . . . . . 10 ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))}
284283a1i 11 . . . . . . . . 9 ((𝜑𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}) = {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))})
28598adantrr 715 . . . . . . . . . . . . . . . . 17 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℕ0)
286285nn0zd 12525 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℤ)
287286zred 12607 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → Σ𝑖𝑆 (𝑓𝑖) ∈ ℝ)
288125ltp1d 12085 . . . . . . . . . . . . . . . 16 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → 𝑦 < (𝑦 + 1))
289287, 125, 127, 128, 288lelttrd 11313 . . . . . . . . . . . . . . 15 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → Σ𝑖𝑆 (𝑓𝑖) < (𝑦 + 1))
290287, 289ltned 11291 . . . . . . . . . . . . . 14 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → Σ𝑖𝑆 (𝑓𝑖) ≠ (𝑦 + 1))
291290neneqd 2948 . . . . . . . . . . . . 13 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → ¬ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))
292291intnand 489 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → ¬ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))
293 nan 828 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ0) → ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))) ↔ (((𝜑𝑦 ∈ ℕ0) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)) → ¬ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))))
294292, 293mpbir 230 . . . . . . . . . . 11 ((𝜑𝑦 ∈ ℕ0) → ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))))
295294alrimiv 1930 . . . . . . . . . 10 ((𝜑𝑦 ∈ ℕ0) → ∀𝑓 ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))))
296 ab0 4334 . . . . . . . . . 10 ({𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))} = ∅ ↔ ∀𝑓 ¬ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))))
297295, 296sylibr 233 . . . . . . . . 9 ((𝜑𝑦 ∈ ℕ0) → {𝑓 ∣ ((𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦) ∧ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1)))} = ∅)
298284, 297eqtrd 2776 . . . . . . . 8 ((𝜑𝑦 ∈ ℕ0) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}) = ∅)
299298adantr 481 . . . . . . 7 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}) = ∅)
300 hashun 14282 . . . . . . 7 (({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∈ Fin ∧ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))} ∈ Fin ∧ ({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∩ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}) = ∅) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))})) = ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))})))
301228, 282, 299, 300syl3anc 1371 . . . . . 6 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))})) = ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))})))
302 simpr 485 . . . . . . . 8 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆)))
303 simplr 767 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑦 ∈ ℕ0)
304 1nn0 12429 . . . . . . . . . . 11 1 ∈ ℕ0
305304a1i 11 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℕ0)
306303, 305nn0addcld 12477 . . . . . . . . 9 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (𝑦 + 1) ∈ ℕ0)
30735ad2antrr 724 . . . . . . . . 9 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑆 ∈ Fin)
30863ad2antrr 724 . . . . . . . . 9 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑆 ≠ ∅)
309 eqid 2736 . . . . . . . . 9 {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))} = {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}
310306, 307, 308, 309sticksstones21 40575 . . . . . . . 8 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))}) = (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)))
311302, 310oveq12d 7375 . . . . . . 7 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))})) = (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))))
312303nn0cnd 12475 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 𝑦 ∈ ℂ)
313 1cnd 11150 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → 1 ∈ ℂ)
31471ad2antrr 724 . . . . . . . . . . . 12 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℂ)
315312, 313, 314ppncand 11552 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + 1) + ((♯‘𝑆) − 1)) = (𝑦 + (♯‘𝑆)))
316315oveq1d 7372 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1)) = ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1)))
317316oveq2d 7373 . . . . . . . . 9 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))))
31882ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℕ0)
319303, 318nn0addcld 12477 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (𝑦 + (♯‘𝑆)) ∈ ℕ0)
320318nn0zd 12525 . . . . . . . . . 10 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘𝑆) ∈ ℤ)
321 bcpasc 14221 . . . . . . . . . 10 (((𝑦 + (♯‘𝑆)) ∈ ℕ0 ∧ (♯‘𝑆) ∈ ℤ) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
322319, 320, 321syl2anc 584 . . . . . . . . 9 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + ((𝑦 + (♯‘𝑆))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
323317, 322eqtrd 2776 . . . . . . . 8 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)))
324312, 314, 313add32d 11382 . . . . . . . . 9 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((𝑦 + (♯‘𝑆)) + 1) = ((𝑦 + 1) + (♯‘𝑆)))
325324oveq1d 7372 . . . . . . . 8 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆)) + 1)C(♯‘𝑆)) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
326323, 325eqtrd 2776 . . . . . . 7 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (((𝑦 + (♯‘𝑆))C(♯‘𝑆)) + (((𝑦 + 1) + ((♯‘𝑆) − 1))C((♯‘𝑆) − 1))) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
327311, 326eqtrd 2776 . . . . . 6 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → ((♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) + (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))})) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
328301, 327eqtrd 2776 . . . . 5 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘({𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)} ∪ {𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) = (𝑦 + 1))})) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
329150, 328eqtrd 2776 . . . 4 (((𝜑𝑦 ∈ ℕ0) ∧ (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑦)}) = ((𝑦 + (♯‘𝑆))C(♯‘𝑆))) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ (𝑦 + 1))}) = (((𝑦 + 1) + (♯‘𝑆))C(♯‘𝑆)))
33011, 18, 25, 32, 92, 329nn0indd 12600 . . 3 ((𝜑𝑁 ∈ ℕ0) → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
3314, 330mpdan 685 . 2 (𝜑 → (♯‘{𝑓 ∣ (𝑓:𝑆⟶ℕ0 ∧ Σ𝑖𝑆 (𝑓𝑖) ≤ 𝑁)}) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
3323, 331eqtrd 2776 1 (𝜑 → (♯‘𝐴) = ((𝑁 + (♯‘𝑆))C(♯‘𝑆)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845  wal 1539   = wceq 1541  wcel 2106  {cab 2713  wne 2943  wral 3064  cdif 3907  cun 3908  cin 3909  wss 3910  c0 4282  𝒫 cpw 4560  {csn 4586   class class class wbr 5105   × cxp 5631   Fn wfn 6491  wf 6492  cfv 6496  (class class class)co 7357  Fincfn 8883  cc 11049  cr 11050  0cc0 11051  1c1 11052   + caddc 11054   < clt 11189  cle 11190  cmin 11385  cn 12153  0cn0 12413  cz 12499  ...cfz 13424  Ccbc 14202  chash 14230  Σcsu 15570
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-inf2 9577  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-inf 9379  df-oi 9446  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-ico 13270  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-fac 14174  df-bc 14203  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator