| Step | Hyp | Ref
| Expression |
| 1 | | ssid 4006 |
. 2
⊢ 𝐴 ⊆ 𝐴 |
| 2 | | fsumiun.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ Fin) |
| 3 | | sseq1 4009 |
. . . . . 6
⊢ (𝑢 = ∅ → (𝑢 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴)) |
| 4 | | iuneq1 5008 |
. . . . . . . . 9
⊢ (𝑢 = ∅ → ∪ 𝑥 ∈ 𝑢 𝐵 = ∪ 𝑥 ∈ ∅ 𝐵) |
| 5 | | 0iun 5063 |
. . . . . . . . 9
⊢ ∪ 𝑥 ∈ ∅ 𝐵 = ∅ |
| 6 | 4, 5 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑢 = ∅ → ∪ 𝑥 ∈ 𝑢 𝐵 = ∅) |
| 7 | 6 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝑢 = ∅ → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑘 ∈ ∅ 𝐶) |
| 8 | | sumeq1 15725 |
. . . . . . 7
⊢ (𝑢 = ∅ → Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘 ∈ 𝐵 𝐶) |
| 9 | 7, 8 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑢 = ∅ → (Σ𝑘 ∈ ∪ 𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶 ↔ Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘 ∈ 𝐵 𝐶)) |
| 10 | 3, 9 | imbi12d 344 |
. . . . 5
⊢ (𝑢 = ∅ → ((𝑢 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶) ↔ (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘 ∈ 𝐵 𝐶))) |
| 11 | 10 | imbi2d 340 |
. . . 4
⊢ (𝑢 = ∅ → ((𝜑 → (𝑢 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶)) ↔ (𝜑 → (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘 ∈ 𝐵 𝐶)))) |
| 12 | | sseq1 4009 |
. . . . . 6
⊢ (𝑢 = 𝑧 → (𝑢 ⊆ 𝐴 ↔ 𝑧 ⊆ 𝐴)) |
| 13 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑢 = 𝑧 → ∪
𝑥 ∈ 𝑢 𝐵 = ∪ 𝑥 ∈ 𝑧 𝐵) |
| 14 | 13 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝑢 = 𝑧 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶) |
| 15 | | sumeq1 15725 |
. . . . . . 7
⊢ (𝑢 = 𝑧 → Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶) |
| 16 | 14, 15 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑢 = 𝑧 → (Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶 ↔ Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶)) |
| 17 | 12, 16 | imbi12d 344 |
. . . . 5
⊢ (𝑢 = 𝑧 → ((𝑢 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶) ↔ (𝑧 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶))) |
| 18 | 17 | imbi2d 340 |
. . . 4
⊢ (𝑢 = 𝑧 → ((𝜑 → (𝑢 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶)) ↔ (𝜑 → (𝑧 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶)))) |
| 19 | | sseq1 4009 |
. . . . . 6
⊢ (𝑢 = (𝑧 ∪ {𝑤}) → (𝑢 ⊆ 𝐴 ↔ (𝑧 ∪ {𝑤}) ⊆ 𝐴)) |
| 20 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑢 = (𝑧 ∪ {𝑤}) → ∪
𝑥 ∈ 𝑢 𝐵 = ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵) |
| 21 | 20 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝑢 = (𝑧 ∪ {𝑤}) → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶) |
| 22 | | sumeq1 15725 |
. . . . . . 7
⊢ (𝑢 = (𝑧 ∪ {𝑤}) → Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶) |
| 23 | 21, 22 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑢 = (𝑧 ∪ {𝑤}) → (Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶 ↔ Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶)) |
| 24 | 19, 23 | imbi12d 344 |
. . . . 5
⊢ (𝑢 = (𝑧 ∪ {𝑤}) → ((𝑢 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶) ↔ ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶))) |
| 25 | 24 | imbi2d 340 |
. . . 4
⊢ (𝑢 = (𝑧 ∪ {𝑤}) → ((𝜑 → (𝑢 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶)) ↔ (𝜑 → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶)))) |
| 26 | | sseq1 4009 |
. . . . . 6
⊢ (𝑢 = 𝐴 → (𝑢 ⊆ 𝐴 ↔ 𝐴 ⊆ 𝐴)) |
| 27 | | iuneq1 5008 |
. . . . . . . 8
⊢ (𝑢 = 𝐴 → ∪
𝑥 ∈ 𝑢 𝐵 = ∪ 𝑥 ∈ 𝐴 𝐵) |
| 28 | 27 | sumeq1d 15736 |
. . . . . . 7
⊢ (𝑢 = 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶) |
| 29 | | sumeq1 15725 |
. . . . . . 7
⊢ (𝑢 = 𝐴 → Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶) |
| 30 | 28, 29 | eqeq12d 2753 |
. . . . . 6
⊢ (𝑢 = 𝐴 → (Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶 ↔ Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)) |
| 31 | 26, 30 | imbi12d 344 |
. . . . 5
⊢ (𝑢 = 𝐴 → ((𝑢 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶) ↔ (𝐴 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶))) |
| 32 | 31 | imbi2d 340 |
. . . 4
⊢ (𝑢 = 𝐴 → ((𝜑 → (𝑢 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑢 𝐵𝐶 = Σ𝑥 ∈ 𝑢 Σ𝑘 ∈ 𝐵 𝐶)) ↔ (𝜑 → (𝐴 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)))) |
| 33 | | sum0 15757 |
. . . . . 6
⊢
Σ𝑘 ∈
∅ 𝐶 =
0 |
| 34 | | sum0 15757 |
. . . . . 6
⊢
Σ𝑥 ∈
∅ Σ𝑘 ∈
𝐵 𝐶 = 0 |
| 35 | 33, 34 | eqtr4i 2768 |
. . . . 5
⊢
Σ𝑘 ∈
∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘 ∈ 𝐵 𝐶 |
| 36 | 35 | 2a1i 12 |
. . . 4
⊢ (𝜑 → (∅ ⊆ 𝐴 → Σ𝑘 ∈ ∅ 𝐶 = Σ𝑥 ∈ ∅ Σ𝑘 ∈ 𝐵 𝐶)) |
| 37 | | id 22 |
. . . . . . . . . 10
⊢ ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (𝑧 ∪ {𝑤}) ⊆ 𝐴) |
| 38 | 37 | unssad 4193 |
. . . . . . . . 9
⊢ ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → 𝑧 ⊆ 𝐴) |
| 39 | 38 | imim1i 63 |
. . . . . . . 8
⊢ ((𝑧 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶)) |
| 40 | | oveq1 7438 |
. . . . . . . . . . 11
⊢
(Σ𝑘 ∈
∪ 𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶 → (Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 + Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶) = (Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶)) |
| 41 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑧𝐵 |
| 42 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥⦋𝑧 / 𝑥⦌𝐵 |
| 43 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑧 → 𝐵 = ⦋𝑧 / 𝑥⦌𝐵) |
| 44 | 41, 42, 43 | cbviun 5036 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑥 ∈ {𝑤}𝐵 = ∪ 𝑧 ∈ {𝑤}⦋𝑧 / 𝑥⦌𝐵 |
| 45 | | vex 3484 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑤 ∈ V |
| 46 | | csbeq1 3902 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑤 → ⦋𝑧 / 𝑥⦌𝐵 = ⦋𝑤 / 𝑥⦌𝐵) |
| 47 | 45, 46 | iunxsn 5091 |
. . . . . . . . . . . . . . . 16
⊢ ∪ 𝑧 ∈ {𝑤}⦋𝑧 / 𝑥⦌𝐵 = ⦋𝑤 / 𝑥⦌𝐵 |
| 48 | 44, 47 | eqtri 2765 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ {𝑤}𝐵 = ⦋𝑤 / 𝑥⦌𝐵 |
| 49 | 48 | ineq2i 4217 |
. . . . . . . . . . . . . 14
⊢ (∪ 𝑥 ∈ 𝑧 𝐵 ∩ ∪
𝑥 ∈ {𝑤}𝐵) = (∪
𝑥 ∈ 𝑧 𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) |
| 50 | | fsumiun.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → Disj 𝑥 ∈ 𝐴 𝐵) |
| 51 | 50 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Disj 𝑥 ∈ 𝐴 𝐵) |
| 52 | 38 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑧 ⊆ 𝐴) |
| 53 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) ⊆ 𝐴) |
| 54 | 53 | unssbd 4194 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → {𝑤} ⊆ 𝐴) |
| 55 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ¬ 𝑤 ∈ 𝑧) |
| 56 | | disjsn 4711 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∩ {𝑤}) = ∅ ↔ ¬ 𝑤 ∈ 𝑧) |
| 57 | 55, 56 | sylibr 234 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∩ {𝑤}) = ∅) |
| 58 | | disjiun 5131 |
. . . . . . . . . . . . . . 15
⊢
((Disj 𝑥
∈ 𝐴 𝐵 ∧ (𝑧 ⊆ 𝐴 ∧ {𝑤} ⊆ 𝐴 ∧ (𝑧 ∩ {𝑤}) = ∅)) → (∪ 𝑥 ∈ 𝑧 𝐵 ∩ ∪
𝑥 ∈ {𝑤}𝐵) = ∅) |
| 59 | 51, 52, 54, 57, 58 | syl13anc 1374 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (∪ 𝑥 ∈ 𝑧 𝐵 ∩ ∪
𝑥 ∈ {𝑤}𝐵) = ∅) |
| 60 | 49, 59 | eqtr3id 2791 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (∪ 𝑥 ∈ 𝑧 𝐵 ∩ ⦋𝑤 / 𝑥⦌𝐵) = ∅) |
| 61 | | iunxun 5094 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = (∪
𝑥 ∈ 𝑧 𝐵 ∪ ∪
𝑥 ∈ {𝑤}𝐵) |
| 62 | 48 | uneq2i 4165 |
. . . . . . . . . . . . . . 15
⊢ (∪ 𝑥 ∈ 𝑧 𝐵 ∪ ∪
𝑥 ∈ {𝑤}𝐵) = (∪
𝑥 ∈ 𝑧 𝐵 ∪ ⦋𝑤 / 𝑥⦌𝐵) |
| 63 | 61, 62 | eqtri 2765 |
. . . . . . . . . . . . . 14
⊢ ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = (∪
𝑥 ∈ 𝑧 𝐵 ∪ ⦋𝑤 / 𝑥⦌𝐵) |
| 64 | 63 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 = (∪
𝑥 ∈ 𝑧 𝐵 ∪ ⦋𝑤 / 𝑥⦌𝐵)) |
| 65 | 2 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝐴 ∈ Fin) |
| 66 | 65, 53 | ssfid 9301 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) ∈ Fin) |
| 67 | | fsumiun.2 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) |
| 68 | 67 | ralrimiva 3146 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) |
| 69 | 68 | ad2antrr 726 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 𝐵 ∈ Fin) |
| 70 | | ssralv 4052 |
. . . . . . . . . . . . . . 15
⊢ ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (∀𝑥 ∈ 𝐴 𝐵 ∈ Fin → ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin)) |
| 71 | 53, 69, 70 | sylc 65 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin) |
| 72 | | iunfi 9383 |
. . . . . . . . . . . . . 14
⊢ (((𝑧 ∪ {𝑤}) ∈ Fin ∧ ∀𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin) → ∪ 𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin) |
| 73 | 66, 71, 72 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ∈ Fin) |
| 74 | | iunss1 5006 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
| 75 | 74 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵 ⊆ ∪
𝑥 ∈ 𝐴 𝐵) |
| 76 | 75 | sselda 3983 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵) → 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
| 77 | | eliun 4995 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
| 78 | | fsumiun.4 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ ℂ) |
| 79 | 78 | rexlimdvaa 3156 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ ℂ)) |
| 80 | 79 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 → 𝐶 ∈ ℂ)) |
| 81 | 77, 80 | biimtrid 242 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 → 𝐶 ∈ ℂ)) |
| 82 | 81 | imp 406 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ ℂ) |
| 83 | 76, 82 | syldan 591 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵) → 𝐶 ∈ ℂ) |
| 84 | 60, 64, 73, 83 | fsumsplit 15777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = (Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 + Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶)) |
| 85 | | eqidd 2738 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (𝑧 ∪ {𝑤}) = (𝑧 ∪ {𝑤})) |
| 86 | 53 | sselda 3983 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → 𝑥 ∈ 𝐴) |
| 87 | 78 | anassrs 467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
| 88 | 67, 87 | fsumcl 15769 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → Σ𝑘 ∈ 𝐵 𝐶 ∈ ℂ) |
| 89 | 88 | ralrimiva 3146 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 ∈ ℂ) |
| 90 | 89 | ad2antrr 726 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → ∀𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 ∈ ℂ) |
| 91 | 90 | r19.21bi 3251 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥 ∈ 𝐴) → Σ𝑘 ∈ 𝐵 𝐶 ∈ ℂ) |
| 92 | 86, 91 | syldan 591 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) ∧ 𝑥 ∈ (𝑧 ∪ {𝑤})) → Σ𝑘 ∈ 𝐵 𝐶 ∈ ℂ) |
| 93 | 57, 85, 66, 92 | fsumsplit 15777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶 = (Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑥 ∈ {𝑤}Σ𝑘 ∈ 𝐵 𝐶)) |
| 94 | 43 | sumeq1d 15736 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑧 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ ⦋ 𝑧 / 𝑥⦌𝐵𝐶) |
| 95 | | nfcv 2905 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑧Σ𝑘 ∈ 𝐵 𝐶 |
| 96 | | nfcv 2905 |
. . . . . . . . . . . . . . . . 17
⊢
Ⅎ𝑥𝐶 |
| 97 | 42, 96 | nfsum 15727 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥Σ𝑘 ∈ ⦋ 𝑧 / 𝑥⦌𝐵𝐶 |
| 98 | 94, 95, 97 | cbvsum 15731 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑥 ∈
{𝑤}Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ {𝑤}Σ𝑘 ∈ ⦋ 𝑧 / 𝑥⦌𝐵𝐶 |
| 99 | 45 | snss 4785 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∈ 𝐴 ↔ {𝑤} ⊆ 𝐴) |
| 100 | 54, 99 | sylibr 234 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → 𝑤 ∈ 𝐴) |
| 101 | | nfcsb1v 3923 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥⦋𝑤 / 𝑥⦌𝐵 |
| 102 | 101, 96 | nfsum 15727 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶 |
| 103 | 102 | nfel1 2922 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑥Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶 ∈ ℂ |
| 104 | | csbeq1a 3913 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 = 𝑤 → 𝐵 = ⦋𝑤 / 𝑥⦌𝐵) |
| 105 | 104 | sumeq1d 15736 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 = 𝑤 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶) |
| 106 | 105 | eleq1d 2826 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑤 → (Σ𝑘 ∈ 𝐵 𝐶 ∈ ℂ ↔ Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶 ∈ ℂ)) |
| 107 | 103, 106 | rspc 3610 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑤 ∈ 𝐴 → (∀𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 ∈ ℂ → Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶 ∈ ℂ)) |
| 108 | 100, 90, 107 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶 ∈ ℂ) |
| 109 | 46 | sumeq1d 15736 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = 𝑤 → Σ𝑘 ∈ ⦋ 𝑧 / 𝑥⦌𝐵𝐶 = Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶) |
| 110 | 109 | sumsn 15782 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑤 ∈ V ∧ Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶 ∈ ℂ) → Σ𝑧 ∈ {𝑤}Σ𝑘 ∈ ⦋ 𝑧 / 𝑥⦌𝐵𝐶 = Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶) |
| 111 | 45, 108, 110 | sylancr 587 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑧 ∈ {𝑤}Σ𝑘 ∈ ⦋ 𝑧 / 𝑥⦌𝐵𝐶 = Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶) |
| 112 | 98, 111 | eqtrid 2789 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ {𝑤}Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶) |
| 113 | 112 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑥 ∈ {𝑤}Σ𝑘 ∈ 𝐵 𝐶) = (Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶)) |
| 114 | 93, 113 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶 = (Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶)) |
| 115 | 84, 114 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶 ↔ (Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 + Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶) = (Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶 + Σ𝑘 ∈ ⦋ 𝑤 / 𝑥⦌𝐵𝐶))) |
| 116 | 40, 115 | imbitrrid 246 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) ∧ (𝑧 ∪ {𝑤}) ⊆ 𝐴) → (Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶 → Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶)) |
| 117 | 116 | ex 412 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → (Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶 → Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶))) |
| 118 | 117 | a2d 29 |
. . . . . . . 8
⊢ ((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) → (((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶))) |
| 119 | 39, 118 | syl5 34 |
. . . . . . 7
⊢ ((𝜑 ∧ ¬ 𝑤 ∈ 𝑧) → ((𝑧 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶))) |
| 120 | 119 | expcom 413 |
. . . . . 6
⊢ (¬
𝑤 ∈ 𝑧 → (𝜑 → ((𝑧 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶) → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶)))) |
| 121 | 120 | a2d 29 |
. . . . 5
⊢ (¬
𝑤 ∈ 𝑧 → ((𝜑 → (𝑧 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶)) → (𝜑 → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶)))) |
| 122 | 121 | adantl 481 |
. . . 4
⊢ ((𝑧 ∈ Fin ∧ ¬ 𝑤 ∈ 𝑧) → ((𝜑 → (𝑧 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝑧 𝐵𝐶 = Σ𝑥 ∈ 𝑧 Σ𝑘 ∈ 𝐵 𝐶)) → (𝜑 → ((𝑧 ∪ {𝑤}) ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ (𝑧 ∪ {𝑤})𝐵𝐶 = Σ𝑥 ∈ (𝑧 ∪ {𝑤})Σ𝑘 ∈ 𝐵 𝐶)))) |
| 123 | 11, 18, 25, 32, 36, 122 | findcard2s 9205 |
. . 3
⊢ (𝐴 ∈ Fin → (𝜑 → (𝐴 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶))) |
| 124 | 2, 123 | mpcom 38 |
. 2
⊢ (𝜑 → (𝐴 ⊆ 𝐴 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)) |
| 125 | 1, 124 | mpi 20 |
1
⊢ (𝜑 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶) |