Step | Hyp | Ref
| Expression |
1 | | sum0 11280 |
. . . 4
⊢
Σ𝑘 ∈
∅ 𝐵 =
0 |
2 | | fsumf1o.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐹:𝐶–1-1-onto→𝐴) |
3 | | f1oeq2 5403 |
. . . . . . . 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 5420 |
. . . . . 6
⊢ (𝐹:∅–1-1-onto→𝐴 → 𝐹:∅–onto→𝐴) |
7 | | fo00 5449 |
. . . . . . 7
⊢ (𝐹:∅–onto→𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅)) |
8 | 7 | simprbi 273 |
. . . . . 6
⊢ (𝐹:∅–onto→𝐴 → 𝐴 = ∅) |
9 | 5, 6, 8 | 3syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐴 = ∅) |
10 | 9 | sumeq1d 11258 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑘 ∈ ∅ 𝐵) |
11 | | simpr 109 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐶 = ∅) → 𝐶 = ∅) |
12 | 11 | sumeq1d 11258 |
. . . . 5
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑛 ∈ 𝐶 𝐷 = Σ𝑛 ∈ ∅ 𝐷) |
13 | | sum0 11280 |
. . . . 5
⊢
Σ𝑛 ∈
∅ 𝐷 =
0 |
14 | 12, 13 | eqtrdi 2206 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑛 ∈ 𝐶 𝐷 = 0) |
15 | 1, 10, 14 | 3eqtr4a 2216 |
. . 3
⊢ ((𝜑 ∧ 𝐶 = ∅) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |
16 | 15 | ex 114 |
. 2
⊢ (𝜑 → (𝐶 = ∅ → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
17 | | 2fveq3 5472 |
. . . . . . . 8
⊢ (𝑚 = (𝑓‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
18 | | simprl 521 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → (♯‘𝐶) ∈
ℕ) |
19 | | simprr 522 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶) |
20 | | f1of 5413 |
. . . . . . . . . . . 12
⊢ (𝐹:𝐶–1-1-onto→𝐴 → 𝐹:𝐶⟶𝐴) |
21 | 2, 20 | syl 14 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹:𝐶⟶𝐴) |
22 | 21 | ffvelrnda 5601 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → (𝐹‘𝑚) ∈ 𝐴) |
23 | | fsumf1o.5 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℂ) |
24 | 23 | fmpttd 5621 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
25 | 24 | ffvelrnda 5601 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝐹‘𝑚) ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
26 | 22, 25 | syldan 280 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
27 | 26 | adantlr 469 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) ∈ ℂ) |
28 | 2 | adantr 274 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → 𝐹:𝐶–1-1-onto→𝐴) |
29 | | f1oco 5436 |
. . . . . . . . . . . 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 5413 |
. . . . . . . . . . 11
⊢ ((𝐹 ∘ 𝑓):(1...(♯‘𝐶))–1-1-onto→𝐴 → (𝐹 ∘ 𝑓):(1...(♯‘𝐶))⟶𝐴) |
32 | 30, 31 | syl 14 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → (𝐹 ∘ 𝑓):(1...(♯‘𝐶))⟶𝐴) |
33 | | fvco3 5538 |
. . . . . . . . . 10
⊢ (((𝐹 ∘ 𝑓):(1...(♯‘𝐶))⟶𝐴 ∧ 𝑛 ∈ (1...(♯‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
34 | 32, 33 | sylan 281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
35 | | f1of 5413 |
. . . . . . . . . . . 12
⊢ (𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶 → 𝑓:(1...(♯‘𝐶))⟶𝐶) |
36 | 35 | ad2antll 483 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → 𝑓:(1...(♯‘𝐶))⟶𝐶) |
37 | | fvco3 5538 |
. . . . . . . . . . 11
⊢ ((𝑓:(1...(♯‘𝐶))⟶𝐶 ∧ 𝑛 ∈ (1...(♯‘𝐶))) → ((𝐹 ∘ 𝑓)‘𝑛) = (𝐹‘(𝑓‘𝑛))) |
38 | 36, 37 | sylan 281 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → ((𝐹 ∘ 𝑓)‘𝑛) = (𝐹‘(𝑓‘𝑛))) |
39 | 38 | fveq2d 5471 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
40 | 34, 39 | eqtrd 2190 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘(𝑓‘𝑛)))) |
41 | 17, 18, 19, 27, 40 | fsum3 11279 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐶 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐶), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛), 0)))‘(♯‘𝐶))) |
42 | | eqid 2157 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ 𝐴 ↦ 𝐵) = (𝑘 ∈ 𝐴 ↦ 𝐵) |
43 | | fsumf1o.1 |
. . . . . . . . . . . . 13
⊢ (𝑘 = 𝐺 → 𝐵 = 𝐷) |
44 | | fsumf1o.4 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) = 𝐺) |
45 | 21 | ffvelrnda 5601 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → (𝐹‘𝑛) ∈ 𝐴) |
46 | 44, 45 | eqeltrrd 2235 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐺 ∈ 𝐴) |
47 | 43 | eleq1d 2226 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = 𝐺 → (𝐵 ∈ ℂ ↔ 𝐷 ∈ ℂ)) |
48 | 23 | ralrimiva 2530 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
49 | 48 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ∀𝑘 ∈ 𝐴 𝐵 ∈ ℂ) |
50 | 47, 49, 46 | rspcdva 2821 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝐷 ∈ ℂ) |
51 | 42, 43, 46, 50 | fvmptd3 5560 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝐺) = 𝐷) |
52 | 44 | fveq2d 5471 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝐺)) |
53 | | simpr 109 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → 𝑛 ∈ 𝐶) |
54 | | eqid 2157 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ 𝐶 ↦ 𝐷) = (𝑛 ∈ 𝐶 ↦ 𝐷) |
55 | 54 | fvmpt2 5550 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ 𝐶 ∧ 𝐷 ∈ ℂ) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = 𝐷) |
56 | 53, 50, 55 | syl2anc 409 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = 𝐷) |
57 | 51, 52, 56 | 3eqtr4rd 2201 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑛 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛))) |
58 | 57 | ralrimiva 2530 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑛 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛))) |
59 | | nffvmpt1 5478 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑛((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) |
60 | 59 | nfeq1 2309 |
. . . . . . . . . . 11
⊢
Ⅎ𝑛((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)) |
61 | | fveq2 5467 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚)) |
62 | | 2fveq3 5472 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑚 → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
63 | 61, 62 | eqeq12d 2172 |
. . . . . . . . . . 11
⊢ (𝑛 = 𝑚 → (((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) ↔ ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)))) |
64 | 60, 63 | rspc 2810 |
. . . . . . . . . 10
⊢ (𝑚 ∈ 𝐶 → (∀𝑛 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑛) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑛)) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚)))) |
65 | 58, 64 | mpan9 279 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
66 | 65 | adantlr 469 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐶) → ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
67 | 66 | sumeq2dv 11260 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = Σ𝑚 ∈ 𝐶 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘(𝐹‘𝑚))) |
68 | | fveq2 5467 |
. . . . . . . 8
⊢ (𝑚 = ((𝐹 ∘ 𝑓)‘𝑛) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = ((𝑘 ∈ 𝐴 ↦ 𝐵)‘((𝐹 ∘ 𝑓)‘𝑛))) |
69 | 24 | adantr 274 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → (𝑘 ∈ 𝐴 ↦ 𝐵):𝐴⟶ℂ) |
70 | 69 | ffvelrnda 5601 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) ∧ 𝑚 ∈ 𝐴) → ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) ∈ ℂ) |
71 | 68, 18, 30, 70, 34 | fsum3 11279 |
. . . . . . 7
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = (seq1( + , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐶), (((𝑘 ∈ 𝐴 ↦ 𝐵) ∘ (𝐹 ∘ 𝑓))‘𝑛), 0)))‘(♯‘𝐶))) |
72 | 41, 67, 71 | 3eqtr4rd 2201 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚)) |
73 | | sumfct 11266 |
. . . . . . . 8
⊢
(∀𝑘 ∈
𝐴 𝐵 ∈ ℂ → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵) |
74 | 48, 73 | syl 14 |
. . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵) |
75 | 74 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐴 ((𝑘 ∈ 𝐴 ↦ 𝐵)‘𝑚) = Σ𝑘 ∈ 𝐴 𝐵) |
76 | 50 | ralrimiva 2530 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑛 ∈ 𝐶 𝐷 ∈ ℂ) |
77 | | sumfct 11266 |
. . . . . . . 8
⊢
(∀𝑛 ∈
𝐶 𝐷 ∈ ℂ → Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = Σ𝑛 ∈ 𝐶 𝐷) |
78 | 76, 77 | syl 14 |
. . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = Σ𝑛 ∈ 𝐶 𝐷) |
79 | 78 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑚 ∈ 𝐶 ((𝑛 ∈ 𝐶 ↦ 𝐷)‘𝑚) = Σ𝑛 ∈ 𝐶 𝐷) |
80 | 72, 75, 79 | 3eqtr3d 2198 |
. . . . 5
⊢ ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶)) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |
81 | 80 | expr 373 |
. . . 4
⊢ ((𝜑 ∧ (♯‘𝐶) ∈ ℕ) → (𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
82 | 81 | exlimdv 1799 |
. . 3
⊢ ((𝜑 ∧ (♯‘𝐶) ∈ ℕ) →
(∃𝑓 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
83 | 82 | expimpd 361 |
. 2
⊢ (𝜑 → (((♯‘𝐶) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶) → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷)) |
84 | | fsumf1o.2 |
. . 3
⊢ (𝜑 → 𝐶 ∈ Fin) |
85 | | fz1f1o 11267 |
. . 3
⊢ (𝐶 ∈ Fin → (𝐶 = ∅ ∨
((♯‘𝐶) ∈
ℕ ∧ ∃𝑓
𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶))) |
86 | 84, 85 | syl 14 |
. 2
⊢ (𝜑 → (𝐶 = ∅ ∨ ((♯‘𝐶) ∈ ℕ ∧
∃𝑓 𝑓:(1...(♯‘𝐶))–1-1-onto→𝐶))) |
87 | 16, 83, 86 | mpjaod 708 |
1
⊢ (𝜑 → Σ𝑘 ∈ 𝐴 𝐵 = Σ𝑛 ∈ 𝐶 𝐷) |