| Step | Hyp | Ref
| Expression |
| 1 | | esumiun.0 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 2 | | esumiun.1 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
| 3 | 1, 2 | aciunf1 32673 |
. . 3
⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)) |
| 4 | | f1f1orn 6859 |
. . . . . 6
⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
| 5 | 4 | anim1i 615 |
. . . . 5
⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)) |
| 6 | | f1f 6804 |
. . . . . . 7
⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵⟶∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
| 7 | 6 | frnd 6744 |
. . . . . 6
⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
| 8 | 7 | adantr 480 |
. . . . 5
⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
| 9 | 5, 8 | jca 511 |
. . . 4
⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
| 10 | 9 | eximi 1835 |
. . 3
⊢
(∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ∃𝑓((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
| 11 | 3, 10 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑓((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
| 12 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑧(𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
| 13 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑧𝐶 |
| 14 | | nfcsb1v 3923 |
. . . . . 6
⊢
Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶 |
| 15 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑧∪ 𝑗 ∈ 𝐴 𝐵 |
| 16 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑧ran
𝑓 |
| 17 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑧◡𝑓 |
| 18 | | csbeq1a 3913 |
. . . . . 6
⊢ (𝑘 = (2nd ‘𝑧) → 𝐶 = ⦋(2nd
‘𝑧) / 𝑘⦌𝐶) |
| 19 | 2 | ralrimiva 3146 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐵 ∈ 𝑊) |
| 20 | | iunexg 7988 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪
𝑗 ∈ 𝐴 𝐵 ∈ V) |
| 21 | 1, 19, 20 | syl2anc 584 |
. . . . . . 7
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V) |
| 22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V) |
| 23 | | simprl 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
| 24 | | f1ocnv 6860 |
. . . . . . . 8
⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑗 ∈ 𝐴 𝐵) |
| 25 | 23, 24 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑗 ∈ 𝐴 𝐵) |
| 26 | 25 | adantrlr 723 |
. . . . . 6
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑗 ∈ 𝐴 𝐵) |
| 27 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝜑 |
| 28 | | nfcv 2905 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗𝑓 |
| 29 | | nfiu1 5027 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗∪ 𝑗 ∈ 𝐴 𝐵 |
| 30 | 28 | nfrn 5963 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗ran
𝑓 |
| 31 | 28, 29, 30 | nff1o 6846 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 |
| 32 | | nfv 1914 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑗(2nd ‘(𝑓‘𝑙)) = 𝑙 |
| 33 | 29, 32 | nfralw 3311 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙 |
| 34 | 31, 33 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑗(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) |
| 35 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗ran
𝑓 |
| 36 | | nfiu1 5027 |
. . . . . . . . . . 11
⊢
Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) |
| 37 | 35, 36 | nfss 3976 |
. . . . . . . . . 10
⊢
Ⅎ𝑗ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) |
| 38 | 34, 37 | nfan 1899 |
. . . . . . . . 9
⊢
Ⅎ𝑗((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
| 39 | 27, 38 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
| 40 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑗 𝑧 ∈ ran 𝑓 |
| 41 | 39, 40 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑗((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) |
| 42 | | simpr 484 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (𝑓‘𝑘) = 𝑧) |
| 43 | 42 | fveq2d 6910 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = (2nd ‘𝑧)) |
| 44 | | simplr 769 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) |
| 45 | | simp-4r 784 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) |
| 46 | 45 | simpld 494 |
. . . . . . . . . . . . 13
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)) |
| 47 | 46 | simprd 495 |
. . . . . . . . . . . 12
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) |
| 48 | 47 | ad2antrr 726 |
. . . . . . . . . . 11
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) |
| 49 | | 2fveq3 6911 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑘 → (2nd ‘(𝑓‘𝑙)) = (2nd ‘(𝑓‘𝑘))) |
| 50 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑙 = 𝑘 → 𝑙 = 𝑘) |
| 51 | 49, 50 | eqeq12d 2753 |
. . . . . . . . . . . 12
⊢ (𝑙 = 𝑘 → ((2nd ‘(𝑓‘𝑙)) = 𝑙 ↔ (2nd ‘(𝑓‘𝑘)) = 𝑘)) |
| 52 | 51 | rspcva 3620 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∧ ∀𝑙 ∈ ∪
𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (2nd ‘(𝑓‘𝑘)) = 𝑘) |
| 53 | 44, 48, 52 | syl2anc 584 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = 𝑘) |
| 54 | 43, 53 | eqtr3d 2779 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘𝑧) = 𝑘) |
| 55 | 46 | simpld 494 |
. . . . . . . . . . 11
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
| 56 | 55 | ad2antrr 726 |
. . . . . . . . . 10
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓) |
| 57 | | f1ocnvfv1 7296 |
. . . . . . . . . 10
⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘) |
| 58 | 56, 44, 57 | syl2anc 584 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘) |
| 59 | 42 | fveq2d 6910 |
. . . . . . . . 9
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = (◡𝑓‘𝑧)) |
| 60 | 54, 58, 59 | 3eqtr2rd 2784 |
. . . . . . . 8
⊢
(((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘𝑧) = (2nd ‘𝑧)) |
| 61 | | f1ofn 6849 |
. . . . . . . . . 10
⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 → 𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵) |
| 62 | 55, 61 | syl 17 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵) |
| 63 | | simpllr 776 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝑧 ∈ ran 𝑓) |
| 64 | | fvelrnb 6969 |
. . . . . . . . . 10
⊢ (𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵 → (𝑧 ∈ ran 𝑓 ↔ ∃𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)) |
| 65 | 64 | biimpa 476 |
. . . . . . . . 9
⊢ ((𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ran 𝑓) → ∃𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧) |
| 66 | 62, 63, 65 | syl2anc 584 |
. . . . . . . 8
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧) |
| 67 | 60, 66 | r19.29a 3162 |
. . . . . . 7
⊢
(((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (◡𝑓‘𝑧) = (2nd ‘𝑧)) |
| 68 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
| 69 | 68 | sselda 3983 |
. . . . . . . 8
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
| 70 | | eliun 4995 |
. . . . . . . 8
⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑧 ∈ ({𝑗} × 𝐵)) |
| 71 | 69, 70 | sylib 218 |
. . . . . . 7
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → ∃𝑗 ∈ 𝐴 𝑧 ∈ ({𝑗} × 𝐵)) |
| 72 | 41, 67, 71 | r19.29af 3268 |
. . . . . 6
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → (◡𝑓‘𝑧) = (2nd ‘𝑧)) |
| 73 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑗𝑘 |
| 74 | 73, 29 | nfel 2920 |
. . . . . . . . 9
⊢
Ⅎ𝑗 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 |
| 75 | 27, 74 | nfan 1899 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝜑 ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) |
| 76 | | esumiun.2 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
| 77 | 76 | adantllr 719 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
| 78 | | eliun 4995 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↔ ∃𝑗 ∈ 𝐴 𝑘 ∈ 𝐵) |
| 79 | 78 | biimpi 216 |
. . . . . . . . 9
⊢ (𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 → ∃𝑗 ∈ 𝐴 𝑘 ∈ 𝐵) |
| 80 | 79 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) → ∃𝑗 ∈ 𝐴 𝑘 ∈ 𝐵) |
| 81 | 75, 77, 80 | r19.29af 3268 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞)) |
| 82 | 81 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞)) |
| 83 | 12, 13, 14, 15, 16, 17, 18, 22, 26, 72, 82 | esumf1o 34051 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 = Σ*𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
| 84 | 83 | eqcomd 2743 |
. . . 4
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = Σ*𝑘 ∈ ∪
𝑗 ∈ 𝐴 𝐵𝐶) |
| 85 | | vsnex 5434 |
. . . . . . . . . 10
⊢ {𝑗} ∈ V |
| 86 | 85 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → {𝑗} ∈ V) |
| 87 | 86, 2 | xpexd 7771 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ({𝑗} × 𝐵) ∈ V) |
| 88 | 87 | ralrimiva 3146 |
. . . . . . 7
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) |
| 89 | | iunexg 7988 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) |
| 90 | 1, 88, 89 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) |
| 91 | 90 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) |
| 92 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝑧 |
| 93 | 92, 36 | nfel 2920 |
. . . . . . . 8
⊢
Ⅎ𝑗 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) |
| 94 | 27, 93 | nfan 1899 |
. . . . . . 7
⊢
Ⅎ𝑗(𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
| 95 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑗(2nd ‘𝑧) |
| 96 | | nfcv 2905 |
. . . . . . . . 9
⊢
Ⅎ𝑗𝐶 |
| 97 | 95, 96 | nfcsbw 3925 |
. . . . . . . 8
⊢
Ⅎ𝑗⦋(2nd ‘𝑧) / 𝑘⦌𝐶 |
| 98 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑗(0[,]+∞) |
| 99 | 97, 98 | nfel 2920 |
. . . . . . 7
⊢
Ⅎ𝑗⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞) |
| 100 | | simprr 773 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → (2nd ‘𝑧) ∈ 𝐵) |
| 101 | | simplll 775 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝜑) |
| 102 | | simplr 769 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝑗 ∈ 𝐴) |
| 103 | 76 | ralrimiva 3146 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞)) |
| 104 | 101, 102,
103 | syl2anc 584 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞)) |
| 105 | | rspcsbela 4438 |
. . . . . . . 8
⊢
(((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞)) →
⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
| 106 | 100, 104,
105 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
| 107 | | xp1st 8046 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ {𝑗}) |
| 108 | | elsni 4643 |
. . . . . . . . . . . 12
⊢
((1st ‘𝑧) ∈ {𝑗} → (1st ‘𝑧) = 𝑗) |
| 109 | 107, 108 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) = 𝑗) |
| 110 | | xp2nd 8047 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵) |
| 111 | 109, 110 | jca 511 |
. . . . . . . . . 10
⊢ (𝑧 ∈ ({𝑗} × 𝐵) → ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) |
| 112 | 111 | reximi 3084 |
. . . . . . . . 9
⊢
(∃𝑗 ∈
𝐴 𝑧 ∈ ({𝑗} × 𝐵) → ∃𝑗 ∈ 𝐴 ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) |
| 113 | 70, 112 | sylbi 217 |
. . . . . . . 8
⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → ∃𝑗 ∈ 𝐴 ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) |
| 114 | 113 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → ∃𝑗 ∈ 𝐴 ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) |
| 115 | 94, 99, 106, 114 | r19.29af2 3267 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
| 116 | 115 | adantlr 715 |
. . . . 5
⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞)) |
| 117 | | simprr 773 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
| 118 | 117 | adantrlr 723 |
. . . . 5
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
| 119 | 12, 91, 116, 118 | esummono 34055 |
. . . 4
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ≤ Σ*𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
| 120 | 84, 119 | eqbrtrrd 5167 |
. . 3
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
| 121 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑗 ∈ V |
| 122 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑘 ∈ V |
| 123 | 121, 122 | op2ndd 8025 |
. . . . . . . 8
⊢ (𝑧 = 〈𝑗, 𝑘〉 → (2nd ‘𝑧) = 𝑘) |
| 124 | 123 | eqcomd 2743 |
. . . . . . 7
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝑘 = (2nd ‘𝑧)) |
| 125 | 124, 18 | syl 17 |
. . . . . 6
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐶 = ⦋(2nd
‘𝑧) / 𝑘⦌𝐶) |
| 126 | 125 | eqcomd 2743 |
. . . . 5
⊢ (𝑧 = 〈𝑗, 𝑘〉 → ⦋(2nd
‘𝑧) / 𝑘⦌𝐶 = 𝐶) |
| 127 | 76 | anasss 466 |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞)) |
| 128 | 14, 126, 1, 2, 127 | esum2d 34094 |
. . . 4
⊢ (𝜑 → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
| 129 | 128 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶) |
| 130 | 120, 129 | breqtrrd 5171 |
. 2
⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran
𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶) |
| 131 | 11, 130 | exlimddv 1935 |
1
⊢ (𝜑 → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶) |