Step | Hyp | Ref
| Expression |
1 | | fsumiunle.1 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ Fin) |
2 | | fsumiunle.2 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin) |
3 | 1, 2 | aciunf1 29463 |
. . 3
⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)) |
4 | | f1f1orn 6148 |
. . . . . 6
⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
5 | 4 | anim1i 592 |
. . . . 5
⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)) |
6 | | f1f 6101 |
. . . . . . 7
⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵⟶∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
7 | | frn 6053 |
. . . . . . 7
⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵⟶∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
9 | 8 | adantr 481 |
. . . . 5
⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
10 | 5, 9 | jca 554 |
. . . 4
⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
11 | 10 | eximi 1762 |
. . 3
⊢
(∃𝑓(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ∃𝑓((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
12 | 3, 11 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑓((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
13 | | csbeq1a 3542 |
. . . . . . 7
⊢ (𝑘 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑘⦌𝐶) |
14 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵 |
15 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑘∪ 𝑥 ∈ 𝐴 𝐵 |
16 | | nfcv 2764 |
. . . . . . 7
⊢
Ⅎ𝑦𝐶 |
17 | | nfcsb1v 3549 |
. . . . . . 7
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶 |
18 | 13, 14, 15, 16, 17 | cbvsum 14425 |
. . . . . 6
⊢
Σ𝑘 ∈
∪ 𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵⦋𝑦 / 𝑘⦌𝐶 |
19 | | csbeq1 3536 |
. . . . . . 7
⊢ (𝑦 = (2nd ‘𝑧) → ⦋𝑦 / 𝑘⦌𝐶 = ⦋(2nd
‘𝑧) / 𝑘⦌𝐶) |
20 | | snfi 8038 |
. . . . . . . . . . . 12
⊢ {𝑥} ∈ Fin |
21 | | xpfi 8231 |
. . . . . . . . . . . 12
⊢ (({𝑥} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑥} × 𝐵) ∈ Fin) |
22 | 20, 2, 21 | sylancr 695 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({𝑥} × 𝐵) ∈ Fin) |
23 | 22 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin) |
24 | | iunfi 8254 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin) |
25 | 1, 23, 24 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin) |
26 | 25 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin) |
27 | | simprr 796 |
. . . . . . . 8
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
28 | 26, 27 | ssfid 8183 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ran 𝑓 ∈ Fin) |
29 | | simprl 794 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
30 | | f1ocnv 6149 |
. . . . . . . . 9
⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑥 ∈ 𝐴 𝐵) |
31 | 29, 30 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑥 ∈ 𝐴 𝐵) |
32 | 31 | adantrlr 759 |
. . . . . . 7
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑥 ∈ 𝐴 𝐵) |
33 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝜑 |
34 | | nfcv 2764 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝑓 |
35 | | nfiu1 4550 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵 |
36 | 34 | nfrn 5368 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥ran
𝑓 |
37 | 34, 35, 36 | nff1o 6135 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 |
38 | | nfv 1843 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥(2nd ‘(𝑓‘𝑙)) = 𝑙 |
39 | 35, 38 | nfral 2945 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∀𝑙 ∈ ∪
𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙 |
40 | 37, 39 | nfan 1828 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) |
41 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥ran
𝑓 |
42 | | nfiu1 4550 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
43 | 41, 42 | nfss 3596 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
44 | 40, 43 | nfan 1828 |
. . . . . . . . . 10
⊢
Ⅎ𝑥((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
45 | 33, 44 | nfan 1828 |
. . . . . . . . 9
⊢
Ⅎ𝑥(𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
46 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑧 ∈ ran 𝑓 |
47 | 45, 46 | nfan 1828 |
. . . . . . . 8
⊢
Ⅎ𝑥((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) |
48 | | simpr 477 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (𝑓‘𝑘) = 𝑧) |
49 | 48 | fveq2d 6195 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = (2nd ‘𝑧)) |
50 | | simplr 792 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
51 | | simp-4r 807 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) |
52 | 51 | simpld 475 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)) |
53 | 52 | simprd 479 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑙 ∈ ∪
𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) |
54 | 53 | ad2antrr 762 |
. . . . . . . . . . . 12
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → ∀𝑙 ∈ ∪
𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) |
55 | | fveq2 6191 |
. . . . . . . . . . . . . . 15
⊢ (𝑙 = 𝑘 → (𝑓‘𝑙) = (𝑓‘𝑘)) |
56 | 55 | fveq2d 6195 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑘 → (2nd ‘(𝑓‘𝑙)) = (2nd ‘(𝑓‘𝑘))) |
57 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑘 → 𝑙 = 𝑘) |
58 | 56, 57 | eqeq12d 2637 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑘 → ((2nd ‘(𝑓‘𝑙)) = 𝑙 ↔ (2nd ‘(𝑓‘𝑘)) = 𝑘)) |
59 | 58 | rspcva 3307 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑙 ∈ ∪
𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (2nd ‘(𝑓‘𝑘)) = 𝑘) |
60 | 50, 54, 59 | syl2anc 693 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = 𝑘) |
61 | 49, 60 | eqtr3d 2658 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘𝑧) = 𝑘) |
62 | 52 | simpld 475 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
63 | 62 | ad2antrr 762 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
64 | | f1ocnvfv1 6532 |
. . . . . . . . . . 11
⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘) |
65 | 63, 50, 64 | syl2anc 693 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘) |
66 | 48 | fveq2d 6195 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = (◡𝑓‘𝑧)) |
67 | 61, 65, 66 | 3eqtr2rd 2663 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘𝑧) = (2nd ‘𝑧)) |
68 | | f1ofn 6138 |
. . . . . . . . . . 11
⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 → 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵) |
69 | 62, 68 | syl 17 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵) |
70 | | simpllr 799 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑧 ∈ ran 𝑓) |
71 | | fvelrnb 6243 |
. . . . . . . . . . 11
⊢ (𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 → (𝑧 ∈ ran 𝑓 ↔ ∃𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)) |
72 | 71 | biimpa 501 |
. . . . . . . . . 10
⊢ ((𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ran 𝑓) → ∃𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧) |
73 | 69, 70, 72 | syl2anc 693 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∃𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧) |
74 | 67, 73 | r19.29a 3078 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (◡𝑓‘𝑧) = (2nd ‘𝑧)) |
75 | 27 | sselda 3603 |
. . . . . . . . 9
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
76 | | eliun 4524 |
. . . . . . . . 9
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
77 | 75, 76 | sylib 208 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
78 | 47, 74, 77 | r19.29af 3076 |
. . . . . . 7
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → (◡𝑓‘𝑧) = (2nd ‘𝑧)) |
79 | | nfv 1843 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
80 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘ℂ |
81 | 17, 80 | nfel 2777 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ |
82 | 79, 81 | nfim 1825 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ) |
83 | | eleq1w 2684 |
. . . . . . . . . . 11
⊢ (𝑘 = 𝑦 → (𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵 ↔ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵)) |
84 | 83 | anbi2d 740 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑦 → ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵))) |
85 | 13 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑦 → (𝐶 ∈ ℂ ↔ ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)) |
86 | 84, 85 | imbi12d 334 |
. . . . . . . . 9
⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ ℂ) ↔ ((𝜑 ∧ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ))) |
87 | | nfcv 2764 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝑘 |
88 | 87, 35 | nfel 2777 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 |
89 | 33, 88 | nfan 1828 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) |
90 | | fsumiunle.3 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℝ) |
91 | 90 | adantllr 755 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℝ) |
92 | 91 | recnd 10068 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
93 | | eliun 4524 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
94 | 93 | biimpi 206 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
95 | 94 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵) |
96 | 89, 92, 95 | r19.29af 3076 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ ℂ) |
97 | 82, 86, 96 | chvar 2262 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ) |
98 | 97 | adantlr 751 |
. . . . . . 7
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ) |
99 | 19, 28, 32, 78, 98 | fsumf1o 14454 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑦 ∈ ∪
𝑥 ∈ 𝐴 𝐵⦋𝑦 / 𝑘⦌𝐶 = Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
100 | 18, 99 | syl5eq 2668 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
101 | 100 | eqcomd 2628 |
. . . 4
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶) |
102 | | nfcv 2764 |
. . . . . . . . 9
⊢
Ⅎ𝑥𝑧 |
103 | 102, 42 | nfel 2777 |
. . . . . . . 8
⊢
Ⅎ𝑥 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) |
104 | 33, 103 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) |
105 | | xp2nd 7199 |
. . . . . . . . 9
⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
106 | 105 | adantl 482 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (2nd ‘𝑧) ∈ 𝐵) |
107 | 90 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ) |
108 | 107 | adantlr 751 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ) |
109 | 108 | adantr 481 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ) |
110 | | nfcsb1v 3549 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶 |
111 | 110 | nfel1 2779 |
. . . . . . . . . 10
⊢
Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ |
112 | | csbeq1a 3542 |
. . . . . . . . . . 11
⊢ (𝑘 = (2nd ‘𝑧) → 𝐶 = ⦋(2nd
‘𝑧) / 𝑘⦌𝐶) |
113 | 112 | eleq1d 2686 |
. . . . . . . . . 10
⊢ (𝑘 = (2nd ‘𝑧) → (𝐶 ∈ ℝ ↔
⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)) |
114 | 111, 113 | rspc 3303 |
. . . . . . . . 9
⊢
((2nd ‘𝑧) ∈ 𝐵 → (∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ →
⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)) |
115 | 114 | imp 445 |
. . . . . . . 8
⊢
(((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ) →
⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ) |
116 | 106, 109,
115 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 ∈ ℝ) |
117 | 76 | biimpi 206 |
. . . . . . . 8
⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
118 | 117 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵)) |
119 | 104, 116,
118 | r19.29af 3076 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 ∈ ℝ) |
120 | 119 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 ∈ ℝ) |
121 | | xp1st 7198 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (1st ‘𝑧) ∈ {𝑥}) |
122 | | elsni 4194 |
. . . . . . . . . . 11
⊢
((1st ‘𝑧) ∈ {𝑥} → (1st ‘𝑧) = 𝑥) |
123 | 121, 122 | syl 17 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (1st ‘𝑧) = 𝑥) |
124 | 123, 105 | jca 554 |
. . . . . . . . 9
⊢ (𝑧 ∈ ({𝑥} × 𝐵) → ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) |
125 | | simplll 798 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝜑) |
126 | | simplr 792 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝑥 ∈ 𝐴) |
127 | | fsumiunle.4 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 0 ≤ 𝐶) |
128 | 127 | ralrimiva 2966 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶) |
129 | 125, 126,
128 | syl2anc 693 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶) |
130 | 124, 129 | sylan2 491 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶) |
131 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘0 |
132 | | nfcv 2764 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘
≤ |
133 | 131, 132,
110 | nfbr 4699 |
. . . . . . . . . 10
⊢
Ⅎ𝑘0 ≤
⦋(2nd ‘𝑧) / 𝑘⦌𝐶 |
134 | 112 | breq2d 4665 |
. . . . . . . . . 10
⊢ (𝑘 = (2nd ‘𝑧) → (0 ≤ 𝐶 ↔ 0 ≤
⦋(2nd ‘𝑧) / 𝑘⦌𝐶)) |
135 | 133, 134 | rspc 3303 |
. . . . . . . . 9
⊢
((2nd ‘𝑧) ∈ 𝐵 → (∀𝑘 ∈ 𝐵 0 ≤ 𝐶 → 0 ≤
⦋(2nd ‘𝑧) / 𝑘⦌𝐶)) |
136 | 135 | imp 445 |
. . . . . . . 8
⊢
(((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 0 ≤ 𝐶) → 0 ≤
⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
137 | 106, 130,
136 | syl2anc 693 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 0 ≤
⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
138 | 104, 137,
118 | r19.29af 3076 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → 0 ≤
⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
139 | 138 | adantlr 751 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → 0 ≤
⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
140 | 26, 120, 139, 27 | fsumless 14528 |
. . . 4
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ≤ Σ𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
141 | 101, 140 | eqbrtrrd 4677 |
. . 3
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
142 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑦𝐵 |
143 | | nfcv 2764 |
. . . . . . . 8
⊢
Ⅎ𝑘𝐵 |
144 | 13, 142, 143, 16, 17 | cbvsum 14425 |
. . . . . . 7
⊢
Σ𝑘 ∈
𝐵 𝐶 = Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶 |
145 | 144 | a1i 11 |
. . . . . 6
⊢ (𝜑 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶) |
146 | 145 | sumeq2sdv 14435 |
. . . . 5
⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶) |
147 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
148 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
149 | 147, 148 | op2ndd 7179 |
. . . . . . . . 9
⊢ (𝑧 = 〈𝑥, 𝑦〉 → (2nd ‘𝑧) = 𝑦) |
150 | 149 | eqcomd 2628 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑥, 𝑦〉 → 𝑦 = (2nd ‘𝑧)) |
151 | 150 | csbeq1d 3540 |
. . . . . . 7
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ⦋𝑦 / 𝑘⦌𝐶 = ⦋(2nd
‘𝑧) / 𝑘⦌𝐶) |
152 | 151 | eqcomd 2628 |
. . . . . 6
⊢ (𝑧 = 〈𝑥, 𝑦〉 → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 = ⦋𝑦 / 𝑘⦌𝐶) |
153 | | nfv 1843 |
. . . . . . . . 9
⊢
Ⅎ𝑘((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) |
154 | 17 | nfel1 2779 |
. . . . . . . . 9
⊢
Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ |
155 | 153, 154 | nfim 1825 |
. . . . . . . 8
⊢
Ⅎ𝑘(((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ) |
156 | | eleq1w 2684 |
. . . . . . . . . 10
⊢ (𝑘 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵)) |
157 | 156 | anbi2d 740 |
. . . . . . . . 9
⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵))) |
158 | 157, 85 | imbi12d 334 |
. . . . . . . 8
⊢ (𝑘 = 𝑦 → ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) ↔ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ))) |
159 | 90 | recnd 10068 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) |
160 | 155, 158,
159 | chvar 2262 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ) |
161 | 160 | anasss 679 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ) |
162 | 152, 1, 2, 161 | fsum2d 14502 |
. . . . 5
⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶 = Σ𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
163 | 146, 162 | eqtrd 2656 |
. . . 4
⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
164 | 163 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
165 | 141, 164 | breqtrrd 4681 |
. 2
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶) |
166 | 12, 165 | exlimddv 1863 |
1
⊢ (𝜑 → Σ𝑘 ∈ ∪
𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶) |