Step | Hyp | Ref
| Expression |
1 | | sge0xp.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
2 | | snex 4908 |
. . . . . 6
⊢ {𝑗} ∈ V |
3 | 2 | a1i 11 |
. . . . 5
⊢ (𝜑 → {𝑗} ∈ V) |
4 | | sge0xp.b |
. . . . 5
⊢ (𝜑 → 𝐵 ∈ 𝑊) |
5 | | xpexg 6960 |
. . . . 5
⊢ (({𝑗} ∈ V ∧ 𝐵 ∈ 𝑊) → ({𝑗} × 𝐵) ∈ V) |
6 | 3, 4, 5 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ({𝑗} × 𝐵) ∈ V) |
7 | 6 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ({𝑗} × 𝐵) ∈ V) |
8 | | disjsnxp 39239 |
. . . 4
⊢
Disj 𝑗 ∈
𝐴 ({𝑗} × 𝐵) |
9 | 8 | a1i 11 |
. . 3
⊢ (𝜑 → Disj 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
10 | | vex 3203 |
. . . . . . . 8
⊢ 𝑗 ∈ V |
11 | | elsnxp 5677 |
. . . . . . . 8
⊢ (𝑗 ∈ V → (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐵 𝑧 = 〈𝑗, 𝑘〉)) |
12 | 10, 11 | ax-mp 5 |
. . . . . . 7
⊢ (𝑧 ∈ ({𝑗} × 𝐵) ↔ ∃𝑘 ∈ 𝐵 𝑧 = 〈𝑗, 𝑘〉) |
13 | 12 | biimpi 206 |
. . . . . 6
⊢ (𝑧 ∈ ({𝑗} × 𝐵) → ∃𝑘 ∈ 𝐵 𝑧 = 〈𝑗, 𝑘〉) |
14 | 13 | adantl 482 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘 ∈ 𝐵 𝑧 = 〈𝑗, 𝑘〉) |
15 | | sge0xp.1 |
. . . . . . . 8
⊢
Ⅎ𝑘𝜑 |
16 | | nfv 1843 |
. . . . . . . 8
⊢
Ⅎ𝑘 𝑗 ∈ 𝐴 |
17 | 15, 16 | nfan 1828 |
. . . . . . 7
⊢
Ⅎ𝑘(𝜑 ∧ 𝑗 ∈ 𝐴) |
18 | | nfv 1843 |
. . . . . . 7
⊢
Ⅎ𝑘 𝑧 ∈ ({𝑗} × 𝐵) |
19 | 17, 18 | nfan 1828 |
. . . . . 6
⊢
Ⅎ𝑘((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) |
20 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑘 𝐷 ∈
(0[,]+∞) |
21 | | sge0xp.z |
. . . . . . . . . 10
⊢ (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 = 𝐶) |
22 | 21 | 3ad2ant3 1084 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵 ∧ 𝑧 = 〈𝑗, 𝑘〉) → 𝐷 = 𝐶) |
23 | | sge0xp.d |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
24 | 23 | 3expa 1265 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞)) |
25 | 24 | 3adant3 1081 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵 ∧ 𝑧 = 〈𝑗, 𝑘〉) → 𝐶 ∈ (0[,]+∞)) |
26 | 22, 25 | eqeltrd 2701 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵 ∧ 𝑧 = 〈𝑗, 𝑘〉) → 𝐷 ∈ (0[,]+∞)) |
27 | 26 | 3exp 1264 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑘 ∈ 𝐵 → (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 ∈ (0[,]+∞)))) |
28 | 27 | adantr 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (𝑘 ∈ 𝐵 → (𝑧 = 〈𝑗, 𝑘〉 → 𝐷 ∈ (0[,]+∞)))) |
29 | 19, 20, 28 | rexlimd 3026 |
. . . . 5
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (∃𝑘 ∈ 𝐵 𝑧 = 〈𝑗, 𝑘〉 → 𝐷 ∈ (0[,]+∞))) |
30 | 14, 29 | mpd 15 |
. . . 4
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝐷 ∈ (0[,]+∞)) |
31 | 30 | 3impa 1259 |
. . 3
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝐷 ∈ (0[,]+∞)) |
32 | 1, 7, 9, 31 | sge0iunmpt 40635 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↦ 𝐷)) =
(Σ^‘(𝑗 ∈ 𝐴 ↦
(Σ^‘(𝑧 ∈ ({𝑗} × 𝐵) ↦ 𝐷))))) |
33 | | iunxpconst 5175 |
. . . . . 6
⊢ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) = (𝐴 × 𝐵) |
34 | 33 | eqcomi 2631 |
. . . . 5
⊢ (𝐴 × 𝐵) = ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵) |
35 | 34 | a1i 11 |
. . . 4
⊢ (𝜑 → (𝐴 × 𝐵) = ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) |
36 | 35 | mpteq1d 4738 |
. . 3
⊢ (𝜑 → (𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐷) = (𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↦ 𝐷)) |
37 | 36 | fveq2d 6195 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐷)) =
(Σ^‘(𝑧 ∈ ∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↦ 𝐷))) |
38 | | nfv 1843 |
. . . 4
⊢
Ⅎ𝑗𝜑 |
39 | | nfv 1843 |
. . . . . 6
⊢
Ⅎ𝑧(𝜑 ∧ 𝑗 ∈ 𝐴) |
40 | 4 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊) |
41 | | simpr 477 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝑗 ∈ 𝐴) |
42 | | eqid 2622 |
. . . . . . 7
⊢ (𝑖 ∈ 𝐵 ↦ 〈𝑗, 𝑖〉) = (𝑖 ∈ 𝐵 ↦ 〈𝑗, 𝑖〉) |
43 | 41, 42 | projf1o 39386 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑖 ∈ 𝐵 ↦ 〈𝑗, 𝑖〉):𝐵–1-1-onto→({𝑗} × 𝐵)) |
44 | | eqidd 2623 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → (𝑖 ∈ 𝐵 ↦ 〈𝑗, 𝑖〉) = (𝑖 ∈ 𝐵 ↦ 〈𝑗, 𝑖〉)) |
45 | | opeq2 4403 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → 〈𝑗, 𝑖〉 = 〈𝑗, 𝑘〉) |
46 | 45 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑘 ∈ 𝐵) ∧ 𝑖 = 𝑘) → 〈𝑗, 𝑖〉 = 〈𝑗, 𝑘〉) |
47 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 𝑘 ∈ 𝐵) |
48 | | opex 4932 |
. . . . . . . . 9
⊢
〈𝑗, 𝑘〉 ∈ V |
49 | 48 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → 〈𝑗, 𝑘〉 ∈ V) |
50 | 44, 46, 47, 49 | fvmptd 6288 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ 𝐵) → ((𝑖 ∈ 𝐵 ↦ 〈𝑗, 𝑖〉)‘𝑘) = 〈𝑗, 𝑘〉) |
51 | 50 | adantlr 751 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → ((𝑖 ∈ 𝐵 ↦ 〈𝑗, 𝑖〉)‘𝑘) = 〈𝑗, 𝑘〉) |
52 | 39, 17, 21, 40, 43, 51, 30 | sge0f1o 40599 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) →
(Σ^‘(𝑧 ∈ ({𝑗} × 𝐵) ↦ 𝐷)) =
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) |
53 | 52 | eqcomd 2628 |
. . . 4
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) →
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)) =
(Σ^‘(𝑧 ∈ ({𝑗} × 𝐵) ↦ 𝐷))) |
54 | 38, 53 | mpteq2da 4743 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶))) = (𝑗 ∈ 𝐴 ↦
(Σ^‘(𝑧 ∈ ({𝑗} × 𝐵) ↦ 𝐷)))) |
55 | 54 | fveq2d 6195 |
. 2
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) =
(Σ^‘(𝑗 ∈ 𝐴 ↦
(Σ^‘(𝑧 ∈ ({𝑗} × 𝐵) ↦ 𝐷))))) |
56 | 32, 37, 55 | 3eqtr4rd 2667 |
1
⊢ (𝜑 →
(Σ^‘(𝑗 ∈ 𝐴 ↦
(Σ^‘(𝑘 ∈ 𝐵 ↦ 𝐶)))) =
(Σ^‘(𝑧 ∈ (𝐴 × 𝐵) ↦ 𝐷))) |