Step | Hyp | Ref
| Expression |
1 | | sum0 11351 |
. . . 4
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 |
2 | | fsumf1o.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) |
3 | | f1oeq2 5432 |
. . . . . . . 8
⊢ (𝐶 = ∅ → (𝐹:𝐶–1-1-onto→𝐴 ↔ 𝐹:∅–1-1-onto→𝐴)) |
4 | 2, 3 | syl5ibcom 154 |
. . . . . . 7
⊢ (𝜑 → (𝐶 = ∅ → 𝐹:∅–1-1-onto→𝐴)) |
5 | 4 | imp 123 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐹:∅–1-1-onto→𝐴) |
6 | | f1ofo 5449 |
. . . . . 6
⊢ (𝐹:∅–1-1-onto→𝐴 → 𝐹:∅–onto→𝐴) |
7 | | fo00 5478 |
. . . . . . 7
⊢ (𝐹:∅–onto→𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅)) |
8 | 7 | simprbi 273 |
. . . . . 6
⊢ (𝐹:∅–onto→𝐴 → 𝐴 = ∅) |
9 | 5, 6, 8 | 3syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐴 = ∅) |
10 | 9 | sumeq1d 11329 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵) |
11 | | simpr 109 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐶 = ∅) |
12 | 11 | sumeq1d 11329 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑛 ∈ 𝐶 𝐷 = Σ𝑛 ∈ ∅ 𝐷) |
13 | | sum0 11351 |
. . . . 5
⊢
Σ𝑛 ∈
∅ 𝐷 =
0 |
14 | 12, 13 | eqtrdi 2219 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑛 ∈ 𝐶 𝐷 = 0) |
15 | 1, 10, 14 | 3eqtr4a 2229 |
. . 3
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |
16 | 15 | ex 114 |
. 2
⊢ (𝜑 → (𝐶 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
17 | | 2fveq3 5501 |
. . . . . . . 8
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
18 | | simprl 526 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → (♯‘𝐶) ∈
ℕ) |
19 | | simprr 527 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶) |
20 | | f1of 5442 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴) |
21 | 2, 20 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐶⟶𝐴) |
22 | 21 | ffvelrnda 5631 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → (𝐹‘𝑚) ∈ 𝐴) |
23 | | fsumf1o.5 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
24 | 23 | fmpttd 5651 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
25 | 24 | ffvelrnda 5631 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐹‘𝑚) ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
26 | 22, 25 | syldan 280 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
27 | 26 | adantlr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
28 | 2 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → 𝐹:𝐶–1-1-onto→𝐴) |
29 | | f1oco 5465 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐶–1-1-onto→𝐴 ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶) → (𝐹 ∘ 𝑓):(1...(♯‘𝐶))–1-1-onto→𝐴) |
30 | 28, 19, 29 | syl2anc 409 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → (𝐹 ∘ 𝑓):(1...(♯‘𝐶))–1-1-onto→𝐴) |
31 | | f1of 5442 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝑓):(1...(♯‘𝐶))–1-1-onto→𝐴 → (𝐹 ∘ 𝑓):(1...(♯‘𝐶))⟶𝐴) |
32 | 30, 31 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → (𝐹 ∘ 𝑓):(1...(♯‘𝐶))⟶𝐴) |
33 | | fvco3 5567 |
. . . . . . . . . 10
⊢ (((𝐹 ∘ 𝑓):(1...(♯‘𝐶))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
34 | 32, 33 | sylan 281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
35 | | f1of 5442 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶 → 𝑓:(1...(♯‘𝐶))⟶𝐶) |
36 | 35 | ad2antll 488 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → 𝑓:(1...(♯‘𝐶))⟶𝐶) |
37 | | fvco3 5567 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(♯‘𝐶))⟶𝐶 ∧ 𝑛 ∈ (1...(♯‘𝐶))) → ((𝐹 ∘ 𝑓)‘𝑛) = (𝐹‘(𝑓‘𝑛))) |
38 | 36, 37 | sylan 281 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → ((𝐹 ∘ 𝑓)‘𝑛) = (𝐹‘(𝑓‘𝑛))) |
39 | 38 | fveq2d 5500 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
40 | 34, 39 | eqtrd 2203 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
41 | 17, 18, 19, 27, 40 | fsum3 11350 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐶 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐶), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛), 0)))‘(♯‘𝐶))) |
42 | | eqid 2170 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
43 | | fsumf1o.1 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) |
44 | | fsumf1o.4 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) |
45 | 21 | ffvelrnda 5631 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴) |
46 | 44, 45 | eqeltrrd 2248 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴) |
47 | 43 | eleq1d 2239 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐺 → (𝐵 ∈ ℂ ↔ 𝐷 ∈ ℂ)) |
48 | 23 | ralrimiva 2543 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
49 | 48 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
50 | 47, 49, 46 | rspcdva 2839 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ ℂ) |
51 | 42, 43, 46, 50 | fvmptd3 5589 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝐺) = 𝐷) |
52 | 44 | fveq2d 5500 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝐺)) |
53 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝑛 ∈ 𝐶) |
54 | | eqid 2170 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷) |
55 | 54 | fvmpt2 5579 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝐶 ∧ 𝐷 ∈ ℂ) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = 𝐷) |
56 | 53, 50, 55 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = 𝐷) |
57 | 51, 52, 56 | 3eqtr4rd 2214 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛))) |
58 | 57 | ralrimiva 2543 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛))) |
59 | | nffvmpt1 5507 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) |
60 | 59 | nfeq1 2322 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) |
61 | | fveq2 5496 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚)) |
62 | | 2fveq3 5501 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
63 | 61, 62 | eqeq12d 2185 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) ↔ ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)))) |
64 | 60, 63 | rspc 2828 |
. . . . . . . . . 10
⊢ (𝑚 ∈ 𝐶 → (∀𝑛 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)))) |
65 | 58, 64 | mpan9 279 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
66 | 65 | adantlr 474 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
67 | 66 | sumeq2dv 11331 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = Σ𝑚 ∈ 𝐶 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
68 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑚 = ((𝐹 ∘ 𝑓)‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
69 | 24 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
70 | 69 | ffvelrnda 5631 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ) |
71 | 68, 18, 30, 70, 34 | fsum3 11350 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐶), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛), 0)))‘(♯‘𝐶))) |
72 | 41, 67, 71 | 3eqtr4rd 2214 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚)) |
73 | | sumfct 11337 |
. . . . . . . 8
⊢
(∀𝑘 ∈
𝐴 𝐵 ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵) |
74 | 48, 73 | syl 14 |
. . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵) |
75 | 74 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵) |
76 | 50 | ralrimiva 2543 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ 𝐶 𝐷 ∈ ℂ) |
77 | | sumfct 11337 |
. . . . . . . 8
⊢
(∀𝑛 ∈
𝐶 𝐷 ∈ ℂ → Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = Σ𝑛 ∈ 𝐶 𝐷) |
78 | 76, 77 | syl 14 |
. . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = Σ𝑛 ∈ 𝐶 𝐷) |
79 | 78 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = Σ𝑛 ∈ 𝐶 𝐷) |
80 | 72, 75, 79 | 3eqtr3d 2211 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |
81 | 80 | expr 373 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝐶) ∈ ℕ) → (𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
82 | 81 | exlimdv 1812 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝐶) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
83 | 82 | expimpd 361 |
. 2
⊢ (𝜑 → (((♯‘𝐶) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
84 | | fsumf1o.2 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Fin) |
85 | | fz1f1o 11338 |
. . 3
⊢ (𝐶 ∈ Fin → (𝐶 = ∅ ∨
((♯‘𝐶) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶))) |
86 | 84, 85 | syl 14 |
. 2
⊢ (𝜑 → (𝐶 = ∅ ∨ ((♯‘𝐶) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶))) |
87 | 16, 83, 86 | mpjaod 713 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |