Step | Hyp | Ref
| Expression |
1 | | ssid 3624 |
. 2
⊢ 𝐵 ⊆ 𝐵 |
2 | | fsumo1.2 |
. . 3
⊢ (𝜑 → 𝐵 ∈ Fin) |
3 | | sseq1 3626 |
. . . . . 6
⊢ (𝑤 = ∅ → (𝑤 ⊆ 𝐵 ↔ ∅ ⊆ 𝐵)) |
4 | | sumeq1 14419 |
. . . . . . . . 9
⊢ (𝑤 = ∅ → Σ𝑘 ∈ 𝑤 𝐶 = Σ𝑘 ∈ ∅ 𝐶) |
5 | | sum0 14452 |
. . . . . . . . 9
⊢
Σ𝑘 ∈
∅ 𝐶 =
0 |
6 | 4, 5 | syl6eq 2672 |
. . . . . . . 8
⊢ (𝑤 = ∅ → Σ𝑘 ∈ 𝑤 𝐶 = 0) |
7 | 6 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑤 = ∅ → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ 0)) |
8 | 7 | eleq1d 2686 |
. . . . . 6
⊢ (𝑤 = ∅ → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1) ↔ (𝑥 ∈ 𝐴 ↦ 0) ∈
𝑂(1))) |
9 | 3, 8 | imbi12d 334 |
. . . . 5
⊢ (𝑤 = ∅ → ((𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1)) ↔ (∅
⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 0) ∈
𝑂(1)))) |
10 | 9 | imbi2d 330 |
. . . 4
⊢ (𝑤 = ∅ → ((𝜑 → (𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1))) ↔ (𝜑 → (∅ ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 0) ∈
𝑂(1))))) |
11 | | sseq1 3626 |
. . . . . 6
⊢ (𝑤 = 𝑦 → (𝑤 ⊆ 𝐵 ↔ 𝑦 ⊆ 𝐵)) |
12 | | sumeq1 14419 |
. . . . . . . 8
⊢ (𝑤 = 𝑦 → Σ𝑘 ∈ 𝑤 𝐶 = Σ𝑘 ∈ 𝑦 𝐶) |
13 | 12 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑤 = 𝑦 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶)) |
14 | 13 | eleq1d 2686 |
. . . . . 6
⊢ (𝑤 = 𝑦 → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1) ↔ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1))) |
15 | 11, 14 | imbi12d 334 |
. . . . 5
⊢ (𝑤 = 𝑦 → ((𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1)) ↔ (𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1)))) |
16 | 15 | imbi2d 330 |
. . . 4
⊢ (𝑤 = 𝑦 → ((𝜑 → (𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1))) ↔ (𝜑 → (𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1))))) |
17 | | sseq1 3626 |
. . . . . 6
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑤 ⊆ 𝐵 ↔ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) |
18 | | sumeq1 14419 |
. . . . . . . 8
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → Σ𝑘 ∈ 𝑤 𝐶 = Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) |
19 | 18 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶)) |
20 | 19 | eleq1d 2686 |
. . . . . 6
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1) ↔ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ∈ 𝑂(1))) |
21 | 17, 20 | imbi12d 334 |
. . . . 5
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1)) ↔ ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ∈ 𝑂(1)))) |
22 | 21 | imbi2d 330 |
. . . 4
⊢ (𝑤 = (𝑦 ∪ {𝑧}) → ((𝜑 → (𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1))) ↔ (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ∈ 𝑂(1))))) |
23 | | sseq1 3626 |
. . . . . 6
⊢ (𝑤 = 𝐵 → (𝑤 ⊆ 𝐵 ↔ 𝐵 ⊆ 𝐵)) |
24 | | sumeq1 14419 |
. . . . . . . 8
⊢ (𝑤 = 𝐵 → Σ𝑘 ∈ 𝑤 𝐶 = Σ𝑘 ∈ 𝐵 𝐶) |
25 | 24 | mpteq2dv 4745 |
. . . . . . 7
⊢ (𝑤 = 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) = (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶)) |
26 | 25 | eleq1d 2686 |
. . . . . 6
⊢ (𝑤 = 𝐵 → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1) ↔ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ∈ 𝑂(1))) |
27 | 23, 26 | imbi12d 334 |
. . . . 5
⊢ (𝑤 = 𝐵 → ((𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1)) ↔ (𝐵 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ∈ 𝑂(1)))) |
28 | 27 | imbi2d 330 |
. . . 4
⊢ (𝑤 = 𝐵 → ((𝜑 → (𝑤 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑤 𝐶) ∈ 𝑂(1))) ↔ (𝜑 → (𝐵 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ∈ 𝑂(1))))) |
29 | | fsumo1.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ ℝ) |
30 | | 0cn 10032 |
. . . . . 6
⊢ 0 ∈
ℂ |
31 | | o1const 14350 |
. . . . . 6
⊢ ((𝐴 ⊆ ℝ ∧ 0 ∈
ℂ) → (𝑥 ∈
𝐴 ↦ 0) ∈
𝑂(1)) |
32 | 29, 30, 31 | sylancl 694 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ 0) ∈
𝑂(1)) |
33 | 32 | a1d 25 |
. . . 4
⊢ (𝜑 → (∅ ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ 0) ∈
𝑂(1))) |
34 | | ssun1 3776 |
. . . . . . . . . 10
⊢ 𝑦 ⊆ (𝑦 ∪ {𝑧}) |
35 | | sstr 3611 |
. . . . . . . . . 10
⊢ ((𝑦 ⊆ (𝑦 ∪ {𝑧}) ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵) → 𝑦 ⊆ 𝐵) |
36 | 34, 35 | mpan 706 |
. . . . . . . . 9
⊢ ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → 𝑦 ⊆ 𝐵) |
37 | 36 | imim1i 63 |
. . . . . . . 8
⊢ ((𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1))) |
38 | | simprl 794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ¬ 𝑧 ∈ 𝑦) |
39 | | disjsn 4246 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑦 ∩ {𝑧}) = ∅ ↔ ¬ 𝑧 ∈ 𝑦) |
40 | 38, 39 | sylibr 224 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦 ∩ {𝑧}) = ∅) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∩ {𝑧}) = ∅) |
42 | | eqidd 2623 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∪ {𝑧}) = (𝑦 ∪ {𝑧})) |
43 | 2 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → 𝐵 ∈ Fin) |
44 | | simprr 796 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦 ∪ {𝑧}) ⊆ 𝐵) |
45 | | ssfi 8180 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐵 ∈ Fin ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵) → (𝑦 ∪ {𝑧}) ∈ Fin) |
46 | 43, 44, 45 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑦 ∪ {𝑧}) ∈ Fin) |
47 | 46 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (𝑦 ∪ {𝑧}) ∈ Fin) |
48 | 44 | sselda 3603 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑘 ∈ 𝐵) |
49 | 48 | adantlr 751 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝑘 ∈ 𝐵) |
50 | | fsumo1.3 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ 𝑉) |
51 | 50 | anass1rs 849 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ 𝑉) |
52 | | fsumo1.4 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1)) |
53 | 51, 52 | o1mptrcl 14353 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑥 ∈ 𝐴) → 𝐶 ∈ ℂ) |
54 | 53 | an32s 846 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
55 | 54 | adantllr 755 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
56 | 49, 55 | syldan 487 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ (𝑦 ∪ {𝑧})) → 𝐶 ∈ ℂ) |
57 | 41, 42, 47, 56 | fsumsplit 14471 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶 = (Σ𝑘 ∈ 𝑦 𝐶 + Σ𝑘 ∈ {𝑧}𝐶)) |
58 | | nfcv 2764 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑤𝐶 |
59 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑘⦋𝑤 / 𝑘⦌𝐶 |
60 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑤 → 𝐶 = ⦋𝑤 / 𝑘⦌𝐶) |
61 | 58, 59, 60 | cbvsumi 14427 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ𝑘 ∈
{𝑧}𝐶 = Σ𝑤 ∈ {𝑧}⦋𝑤 / 𝑘⦌𝐶 |
62 | 44 | unssbd 3791 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → {𝑧} ⊆ 𝐵) |
63 | | vex 3203 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 𝑧 ∈ V |
64 | 63 | snss 4316 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 ∈ 𝐵 ↔ {𝑧} ⊆ 𝐵) |
65 | 62, 64 | sylibr 224 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → 𝑧 ∈ 𝐵) |
66 | 65 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → 𝑧 ∈ 𝐵) |
67 | 55 | ralrimiva 2966 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ) |
68 | | nfcsb1v 3549 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐶 |
69 | 68 | nfel1 2779 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
Ⅎ𝑘⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ |
70 | | csbeq1a 3542 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑧 → 𝐶 = ⦋𝑧 / 𝑘⦌𝐶) |
71 | 70 | eleq1d 2686 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑧 → (𝐶 ∈ ℂ ↔ ⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ)) |
72 | 69, 71 | rspc 3303 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 ∈ 𝐵 → (∀𝑘 ∈ 𝐵 𝐶 ∈ ℂ → ⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ)) |
73 | 66, 67, 72 | sylc 65 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → ⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ) |
74 | | csbeq1 3536 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = 𝑧 → ⦋𝑤 / 𝑘⦌𝐶 = ⦋𝑧 / 𝑘⦌𝐶) |
75 | 74 | sumsn 14475 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑧 ∈ 𝐵 ∧ ⦋𝑧 / 𝑘⦌𝐶 ∈ ℂ) → Σ𝑤 ∈ {𝑧}⦋𝑤 / 𝑘⦌𝐶 = ⦋𝑧 / 𝑘⦌𝐶) |
76 | 66, 73, 75 | syl2anc 693 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → Σ𝑤 ∈ {𝑧}⦋𝑤 / 𝑘⦌𝐶 = ⦋𝑧 / 𝑘⦌𝐶) |
77 | 61, 76 | syl5eq 2668 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → Σ𝑘 ∈ {𝑧}𝐶 = ⦋𝑧 / 𝑘⦌𝐶) |
78 | 77 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → (Σ𝑘 ∈ 𝑦 𝐶 + Σ𝑘 ∈ {𝑧}𝐶) = (Σ𝑘 ∈ 𝑦 𝐶 + ⦋𝑧 / 𝑘⦌𝐶)) |
79 | 57, 78 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶 = (Σ𝑘 ∈ 𝑦 𝐶 + ⦋𝑧 / 𝑘⦌𝐶)) |
80 | 79 | mpteq2dva 4744 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) = (𝑥 ∈ 𝐴 ↦ (Σ𝑘 ∈ 𝑦 𝐶 + ⦋𝑧 / 𝑘⦌𝐶))) |
81 | 29 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → 𝐴 ⊆ ℝ) |
82 | | reex 10027 |
. . . . . . . . . . . . . . . . 17
⊢ ℝ
∈ V |
83 | 82 | ssex 4802 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ⊆ ℝ → 𝐴 ∈ V) |
84 | 81, 83 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → 𝐴 ∈ V) |
85 | | sumex 14418 |
. . . . . . . . . . . . . . . 16
⊢
Σ𝑘 ∈
𝑦 𝐶 ∈ V |
86 | 85 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ 𝑥 ∈ 𝐴) → Σ𝑘 ∈ 𝑦 𝐶 ∈ V) |
87 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) = (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶)) |
88 | | eqidd 2623 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) = (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶)) |
89 | 84, 86, 73, 87, 88 | offval2 6914 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∘𝑓 + (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶)) = (𝑥 ∈ 𝐴 ↦ (Σ𝑘 ∈ 𝑦 𝐶 + ⦋𝑧 / 𝑘⦌𝐶))) |
90 | 80, 89 | eqtr4d 2659 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) = ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∘𝑓 + (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶))) |
91 | 90 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1)) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) = ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∘𝑓 + (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶))) |
92 | | id 22 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1)) |
93 | 52 | ralrimiva 2966 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑘 ∈ 𝐵 (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1)) |
94 | 93 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ∀𝑘 ∈ 𝐵 (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1)) |
95 | | nfcv 2764 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑘𝐴 |
96 | 95, 68 | nfmpt 4746 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑘(𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) |
97 | 96 | nfel1 2779 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑘(𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) ∈ 𝑂(1) |
98 | 70 | mpteq2dv 4745 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑧 → (𝑥 ∈ 𝐴 ↦ 𝐶) = (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶)) |
99 | 98 | eleq1d 2686 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 = 𝑧 → ((𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1) ↔ (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) ∈ 𝑂(1))) |
100 | 97, 99 | rspc 3303 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ 𝐵 → (∀𝑘 ∈ 𝐵 (𝑥 ∈ 𝐴 ↦ 𝐶) ∈ 𝑂(1) → (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) ∈ 𝑂(1))) |
101 | 65, 94, 100 | sylc 65 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) ∈ 𝑂(1)) |
102 | | o1add 14344 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1) ∧ (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶) ∈ 𝑂(1)) → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∘𝑓 + (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶)) ∈ 𝑂(1)) |
103 | 92, 101, 102 | syl2anr 495 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1)) → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∘𝑓 + (𝑥 ∈ 𝐴 ↦ ⦋𝑧 / 𝑘⦌𝐶)) ∈ 𝑂(1)) |
104 | 91, 103 | eqeltrd 2701 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) ∧ (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1)) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ∈ 𝑂(1)) |
105 | 104 | ex 450 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (¬ 𝑧 ∈ 𝑦 ∧ (𝑦 ∪ {𝑧}) ⊆ 𝐵)) → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ∈ 𝑂(1))) |
106 | 105 | expr 643 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → ((𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1) → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ∈ 𝑂(1)))) |
107 | 106 | a2d 29 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑧 ∈ 𝑦) → (((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ∈ 𝑂(1)))) |
108 | 37, 107 | syl5 34 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑧 ∈ 𝑦) → ((𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ∈ 𝑂(1)))) |
109 | 108 | expcom 451 |
. . . . . 6
⊢ (¬
𝑧 ∈ 𝑦 → (𝜑 → ((𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1)) → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ∈ 𝑂(1))))) |
110 | 109 | a2d 29 |
. . . . 5
⊢ (¬
𝑧 ∈ 𝑦 → ((𝜑 → (𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1))) → (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ∈ 𝑂(1))))) |
111 | 110 | adantl 482 |
. . . 4
⊢ ((𝑦 ∈ Fin ∧ ¬ 𝑧 ∈ 𝑦) → ((𝜑 → (𝑦 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝑦 𝐶) ∈ 𝑂(1))) → (𝜑 → ((𝑦 ∪ {𝑧}) ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ (𝑦 ∪ {𝑧})𝐶) ∈ 𝑂(1))))) |
112 | 10, 16, 22, 28, 33, 111 | findcard2s 8201 |
. . 3
⊢ (𝐵 ∈ Fin → (𝜑 → (𝐵 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ∈ 𝑂(1)))) |
113 | 2, 112 | mpcom 38 |
. 2
⊢ (𝜑 → (𝐵 ⊆ 𝐵 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ∈ 𝑂(1))) |
114 | 1, 113 | mpi 20 |
1
⊢ (𝜑 → (𝑥 ∈ 𝐴 ↦ Σ𝑘 ∈ 𝐵 𝐶) ∈ 𝑂(1)) |