Step | Hyp | Ref
| Expression |
1 | | esumiun.0 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | esumiun.1 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
3 | 1, 2 | aciunf1 28845 |
. . 3
⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)) |
4 | | f1f1orn 6061 |
. . . . . 6
⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
5 | 4 | anim1i 590 |
. . . . 5
⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)) |
6 | | f1f 6014 |
. . . . . . 7
⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵⟶∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
7 | | frn 5966 |
. . . . . . 7
⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵⟶∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
8 | 6, 7 | syl 17 |
. . . . . 6
⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
9 | 8 | adantr 480 |
. . . . 5
⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
10 | 5, 9 | jca 553 |
. . . 4
⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
11 | 10 | eximi 1752 |
. . 3
⊢
(∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ∃𝑓((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
12 | 3, 11 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑓((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
13 | | nfv 1830 |
. . . . . 6
⊢
Ⅎ𝑧(𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
14 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑧𝐶 |
15 | | nfcsb1v 3515 |
. . . . . 6
⊢
Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶 |
16 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑧∪ 𝑗 ∈ 𝐴 𝐵 |
17 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑧ran
𝑓 |
18 | | nfcv 2751 |
. . . . . 6
⊢
Ⅎ𝑧◡𝑓 |
19 | | csbeq1a 3508 |
. . . . . 6
⊢ (𝑘 = (2nd ‘𝑧) → 𝐶 = ⦋(2nd
‘𝑧) / 𝑘⦌𝐶) |
20 | 2 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐵 ∈ 𝑊) |
21 | | iunexg 7035 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪
𝑗 ∈ 𝐴 𝐵 ∈ V) |
22 | 1, 20, 21 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V) |
23 | 22 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V) |
24 | | simprl 790 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
25 | | f1ocnv 6062 |
. . . . . . . 8
⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑗 ∈ 𝐴 𝐵) |
26 | 24, 25 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑗 ∈ 𝐴 𝐵) |
27 | 26 | adantrlr 755 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑗 ∈ 𝐴 𝐵) |
28 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝜑 |
29 | | nfcv 2751 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗𝑓 |
30 | | nfiu1 4486 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗∪ 𝑗 ∈ 𝐴 𝐵 |
31 | 29 | nfrn 5289 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗ran
𝑓 |
32 | 29, 30, 31 | nff1o 6048 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 |
33 | | nfv 1830 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗(2nd ‘(𝑓‘𝑙)) = 𝑙 |
34 | 30, 33 | nfral 2929 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙 |
35 | 32, 34 | nfan 1816 |
. . . . . . . . . 10
⊢
Ⅎ𝑗(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) |
36 | | nfcv 2751 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗ran
𝑓 |
37 | | nfiu1 4486 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) |
38 | 36, 37 | nfss 3561 |
. . . . . . . . . 10
⊢
Ⅎ𝑗ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) |
39 | 35, 38 | nfan 1816 |
. . . . . . . . 9
⊢
Ⅎ𝑗((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
40 | 28, 39 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
41 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑗 𝑧 ∈ ran 𝑓 |
42 | 40, 41 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑗((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) |
43 | | simpr 476 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (𝑓‘𝑘) = 𝑧) |
44 | 43 | fveq2d 6107 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = (2nd ‘𝑧)) |
45 | | simplr 788 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) |
46 | | simp-4r 803 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
47 | 46 | simpld 474 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)) |
48 | 47 | simprd 478 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) |
49 | 48 | ad2antrr 758 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) |
50 | | fveq2 6103 |
. . . . . . . . . . . . . 14
⊢ (𝑙 = 𝑘 → (𝑓‘𝑙) = (𝑓‘𝑘)) |
51 | 50 | fveq2d 6107 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑘 → (2nd ‘(𝑓‘𝑙)) = (2nd ‘(𝑓‘𝑘))) |
52 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑘 → 𝑙 = 𝑘) |
53 | 51, 52 | eqeq12d 2625 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑘 → ((2nd ‘(𝑓‘𝑙)) = 𝑙 ↔ (2nd ‘(𝑓‘𝑘)) = 𝑘)) |
54 | 53 | rspcva 3280 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (2nd ‘(𝑓‘𝑘)) = 𝑘) |
55 | 45, 49, 54 | syl2anc 691 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = 𝑘) |
56 | 44, 55 | eqtr3d 2646 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘𝑧) = 𝑘) |
57 | 47 | simpld 474 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
58 | 57 | ad2antrr 758 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
59 | | f1ocnvfv1 6432 |
. . . . . . . . . 10
⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘) |
60 | 58, 45, 59 | syl2anc 691 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘) |
61 | 43 | fveq2d 6107 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = (◡𝑓‘𝑧)) |
62 | 56, 60, 61 | 3eqtr2rd 2651 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘𝑧) = (2nd ‘𝑧)) |
63 | | f1ofn 6051 |
. . . . . . . . . 10
⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 → 𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵) |
64 | 57, 63 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵) |
65 | | simpllr 795 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝑧 ∈ ran 𝑓) |
66 | | fvelrnb 6153 |
. . . . . . . . . 10
⊢ (𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵 → (𝑧 ∈ ran 𝑓 ↔ ∃𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)) |
67 | 66 | biimpa 500 |
. . . . . . . . 9
⊢ ((𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ran 𝑓) → ∃𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧) |
68 | 64, 65, 67 | syl2anc 691 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧) |
69 | 62, 68 | r19.29a 3060 |
. . . . . . 7
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (◡𝑓‘𝑧) = (2nd ‘𝑧)) |
70 | | simprr 792 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
71 | 70 | sselda 3568 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
72 | | eliun 4460 |
. . . . . . . 8
⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑧 ∈ ({𝑗} × 𝐵)) |
73 | 71, 72 | sylib 207 |
. . . . . . 7
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → ∃𝑗 ∈ 𝐴 𝑧 ∈ ({𝑗} × 𝐵)) |
74 | 42, 69, 73 | r19.29af 3058 |
. . . . . 6
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → (◡𝑓‘𝑧) = (2nd ‘𝑧)) |
75 | | nfcv 2751 |
. . . . . . . . . 10
⊢
Ⅎ𝑗𝑘 |
76 | 75, 30 | nfel 2763 |
. . . . . . . . 9
⊢
Ⅎ𝑗 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 |
77 | 28, 76 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝜑 ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) |
78 | | esumiun.2 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
79 | 78 | adantllr 751 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
80 | | eliun 4460 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↔ ∃𝑗 ∈ 𝐴 𝑘 ∈ 𝐵) |
81 | 80 | biimpi 205 |
. . . . . . . . 9
⊢ (𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ∃𝑗 ∈ 𝐴 𝑘 ∈ 𝐵) |
82 | 81 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) → ∃𝑗 ∈ 𝐴 𝑘 ∈ 𝐵) |
83 | 77, 79, 82 | r19.29af 3058 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞)) |
84 | 83 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞)) |
85 | 13, 14, 15, 16, 17, 18, 19, 23, 27, 74, 84 | esumf1o 29439 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 = Σ*𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
86 | 85 | eqcomd 2616 |
. . . 4
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = Σ*𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵𝐶) |
87 | | snex 4835 |
. . . . . . . . . 10
⊢ {𝑗} ∈ V |
88 | 87 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → {𝑗} ∈ V) |
89 | | xpexg 6858 |
. . . . . . . . 9
⊢ (({𝑗} ∈ V ∧ 𝐵 ∈ 𝑊) → ({𝑗} × 𝐵) ∈ V) |
90 | 88, 2, 89 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ({𝑗} × 𝐵) ∈ V) |
91 | 90 | ralrimiva 2949 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) |
92 | | iunexg 7035 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) |
93 | 1, 91, 92 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) |
94 | 93 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) |
95 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝑧 |
96 | 95, 37 | nfel 2763 |
. . . . . . . 8
⊢
Ⅎ𝑗 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) |
97 | 28, 96 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑗(𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
98 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑗(2nd ‘𝑧) |
99 | | nfcv 2751 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝐶 |
100 | 98, 99 | nfcsb 3517 |
. . . . . . . 8
⊢
Ⅎ𝑗⦋(2nd ‘𝑧) / 𝑘⦌𝐶 |
101 | | nfcv 2751 |
. . . . . . . 8
⊢
Ⅎ𝑗(0[,]+∞) |
102 | 100, 101 | nfel 2763 |
. . . . . . 7
⊢
Ⅎ𝑗⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞) |
103 | | simprr 792 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → (2nd ‘𝑧) ∈ 𝐵) |
104 | | simplll 794 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝜑) |
105 | | simplr 788 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝑗 ∈ 𝐴) |
106 | 78 | ralrimiva 2949 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞)) |
107 | 104, 105,
106 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞)) |
108 | | rspcsbela 3958 |
. . . . . . . 8
⊢
(((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞)) →
⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
109 | 103, 107,
108 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
110 | | xp1st 7089 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ {𝑗}) |
111 | | elsni 4142 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑧) ∈ {𝑗} → (1st ‘𝑧) = 𝑗) |
112 | 110, 111 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) = 𝑗) |
113 | | xp2nd 7090 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
114 | 112, 113 | jca 553 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ({𝑗} × 𝐵) → ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) |
115 | 114 | reximi 2994 |
. . . . . . . . 9
⊢
(∃𝑗 ∈
𝐴 𝑧 ∈ ({𝑗} × 𝐵) → ∃𝑗 ∈ 𝐴 ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) |
116 | 72, 115 | sylbi 206 |
. . . . . . . 8
⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → ∃𝑗 ∈ 𝐴 ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) |
117 | 116 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → ∃𝑗 ∈ 𝐴 ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) |
118 | 97, 102, 109, 117 | r19.29af2 3057 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
119 | 118 | adantlr 747 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
120 | | simprr 792 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
121 | 120 | adantrlr 755 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
122 | 13, 94, 119, 121 | esummono 29443 |
. . . 4
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ≤ Σ*𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
123 | 86, 122 | eqbrtrrd 4607 |
. . 3
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
124 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑗 ∈ V |
125 | | vex 3176 |
. . . . . . . . 9
⊢ 𝑘 ∈ V |
126 | 124, 125 | op2ndd 7070 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑗, 𝑘〉 → (2nd ‘𝑧) = 𝑘) |
127 | 126 | eqcomd 2616 |
. . . . . . 7
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝑘 = (2nd ‘𝑧)) |
128 | 127, 19 | syl 17 |
. . . . . 6
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐶 = ⦋(2nd
‘𝑧) / 𝑘⦌𝐶) |
129 | 128 | eqcomd 2616 |
. . . . 5
⊢ (𝑧 = 〈𝑗, 𝑘〉 → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 = 𝐶) |
130 | 78 | anasss 677 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞)) |
131 | 15, 129, 1, 2, 130 | esum2d 29482 |
. . . 4
⊢ (𝜑 → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
132 | 131 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
133 | 123, 132 | breqtrrd 4611 |
. 2
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶) |
134 | 12, 133 | exlimddv 1850 |
1
⊢ (𝜑 → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶) |