Step |
Hyp |
Ref |
Expression |
1 |
|
sge0xp.1 |
⊢ Ⅎ 𝑘 𝜑 |
2 |
|
sge0xp.z |
⊢ ( 𝑧 = 〈 𝑗 , 𝑘 〉 → 𝐷 = 𝐶 ) |
3 |
|
sge0xp.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
4 |
|
sge0xp.b |
⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) |
5 |
|
sge0xp.d |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) ) |
6 |
|
snex |
⊢ { 𝑗 } ∈ V |
7 |
6
|
a1i |
⊢ ( 𝜑 → { 𝑗 } ∈ V ) |
8 |
7 4
|
xpexd |
⊢ ( 𝜑 → ( { 𝑗 } × 𝐵 ) ∈ V ) |
9 |
8
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( { 𝑗 } × 𝐵 ) ∈ V ) |
10 |
|
disjsnxp |
⊢ Disj 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) |
11 |
10
|
a1i |
⊢ ( 𝜑 → Disj 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) |
12 |
|
vex |
⊢ 𝑗 ∈ V |
13 |
|
elsnxp |
⊢ ( 𝑗 ∈ V → ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑘 ∈ 𝐵 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) |
14 |
12 13
|
ax-mp |
⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑘 ∈ 𝐵 𝑧 = 〈 𝑗 , 𝑘 〉 ) |
15 |
14
|
biimpi |
⊢ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) → ∃ 𝑘 ∈ 𝐵 𝑧 = 〈 𝑗 , 𝑘 〉 ) |
16 |
15
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑘 ∈ 𝐵 𝑧 = 〈 𝑗 , 𝑘 〉 ) |
17 |
|
nfv |
⊢ Ⅎ 𝑘 𝑗 ∈ 𝐴 |
18 |
1 17
|
nfan |
⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) |
19 |
|
nfv |
⊢ Ⅎ 𝑘 𝑧 ∈ ( { 𝑗 } × 𝐵 ) |
20 |
18 19
|
nfan |
⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) |
21 |
|
nfv |
⊢ Ⅎ 𝑘 𝐷 ∈ ( 0 [,] +∞ ) |
22 |
2
|
3ad2ant3 |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) → 𝐷 = 𝐶 ) |
23 |
5
|
3expa |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) ) |
24 |
23
|
3adant3 |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) → 𝐶 ∈ ( 0 [,] +∞ ) ) |
25 |
22 24
|
eqeltrd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) → 𝐷 ∈ ( 0 [,] +∞ ) ) |
26 |
25
|
3exp |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑘 ∈ 𝐵 → ( 𝑧 = 〈 𝑗 , 𝑘 〉 → 𝐷 ∈ ( 0 [,] +∞ ) ) ) ) |
27 |
26
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( 𝑘 ∈ 𝐵 → ( 𝑧 = 〈 𝑗 , 𝑘 〉 → 𝐷 ∈ ( 0 [,] +∞ ) ) ) ) |
28 |
20 21 27
|
rexlimd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ( ∃ 𝑘 ∈ 𝐵 𝑧 = 〈 𝑗 , 𝑘 〉 → 𝐷 ∈ ( 0 [,] +∞ ) ) ) |
29 |
16 28
|
mpd |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝐷 ∈ ( 0 [,] +∞ ) ) |
30 |
29
|
3impa |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝐷 ∈ ( 0 [,] +∞ ) ) |
31 |
3 9 11 30
|
sge0iunmpt |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) = ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) ) ) ) |
32 |
|
iunxpconst |
⊢ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) = ( 𝐴 × 𝐵 ) |
33 |
32
|
eqcomi |
⊢ ( 𝐴 × 𝐵 ) = ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) |
34 |
33
|
a1i |
⊢ ( 𝜑 → ( 𝐴 × 𝐵 ) = ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) |
35 |
34
|
mpteq1d |
⊢ ( 𝜑 → ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐷 ) = ( 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) |
36 |
35
|
fveq2d |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐷 ) ) = ( Σ^ ‘ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) ) |
37 |
|
nfv |
⊢ Ⅎ 𝑗 𝜑 |
38 |
|
nfv |
⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) |
39 |
4
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 ) |
40 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝑗 ∈ 𝐴 ) |
41 |
|
eqid |
⊢ ( 𝑖 ∈ 𝐵 ↦ 〈 𝑗 , 𝑖 〉 ) = ( 𝑖 ∈ 𝐵 ↦ 〈 𝑗 , 𝑖 〉 ) |
42 |
40 41
|
projf1o |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( 𝑖 ∈ 𝐵 ↦ 〈 𝑗 , 𝑖 〉 ) : 𝐵 –1-1-onto→ ( { 𝑗 } × 𝐵 ) ) |
43 |
|
eqidd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( 𝑖 ∈ 𝐵 ↦ 〈 𝑗 , 𝑖 〉 ) = ( 𝑖 ∈ 𝐵 ↦ 〈 𝑗 , 𝑖 〉 ) ) |
44 |
|
opeq2 |
⊢ ( 𝑖 = 𝑘 → 〈 𝑗 , 𝑖 〉 = 〈 𝑗 , 𝑘 〉 ) |
45 |
44
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑖 = 𝑘 ) → 〈 𝑗 , 𝑖 〉 = 〈 𝑗 , 𝑘 〉 ) |
46 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 ) |
47 |
|
opex |
⊢ 〈 𝑗 , 𝑘 〉 ∈ V |
48 |
47
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → 〈 𝑗 , 𝑘 〉 ∈ V ) |
49 |
43 45 46 48
|
fvmptd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝐵 ↦ 〈 𝑗 , 𝑖 〉 ) ‘ 𝑘 ) = 〈 𝑗 , 𝑘 〉 ) |
50 |
49
|
adantlr |
⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → ( ( 𝑖 ∈ 𝐵 ↦ 〈 𝑗 , 𝑖 〉 ) ‘ 𝑘 ) = 〈 𝑗 , 𝑘 〉 ) |
51 |
38 18 2 39 42 50 29
|
sge0f1o |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) = ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) |
52 |
51
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) = ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) ) |
53 |
37 52
|
mpteq2da |
⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) = ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) ) ) |
54 |
53
|
fveq2d |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↦ 𝐷 ) ) ) ) ) |
55 |
31 36 54
|
3eqtr4rd |
⊢ ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ 𝐴 ↦ ( Σ^ ‘ ( 𝑘 ∈ 𝐵 ↦ 𝐶 ) ) ) ) = ( Σ^ ‘ ( 𝑧 ∈ ( 𝐴 × 𝐵 ) ↦ 𝐷 ) ) ) |