Step |
Hyp |
Ref |
Expression |
1 |
|
gsum2d2.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
gsum2d2.z |
⊢ 0 = ( 0g ‘ 𝐺 ) |
3 |
|
gsum2d2.g |
⊢ ( 𝜑 → 𝐺 ∈ CMnd ) |
4 |
|
gsum2d2.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
5 |
|
gsum2d2.r |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑊 ) |
6 |
|
gsum2d2.f |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → 𝑋 ∈ 𝐵 ) |
7 |
|
gsum2d2.u |
⊢ ( 𝜑 → 𝑈 ∈ Fin ) |
8 |
|
gsum2d2.n |
⊢ ( ( 𝜑 ∧ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) ) → 𝑋 = 0 ) |
9 |
|
gsumcom2.d |
⊢ ( 𝜑 → 𝐷 ∈ 𝑌 ) |
10 |
|
gsumcom2.c |
⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ↔ ( 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸 ) ) ) |
11 |
|
snex |
⊢ { 𝑗 } ∈ V |
12 |
|
xpexg |
⊢ ( ( { 𝑗 } ∈ V ∧ 𝐶 ∈ 𝑊 ) → ( { 𝑗 } × 𝐶 ) ∈ V ) |
13 |
11 5 12
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( { 𝑗 } × 𝐶 ) ∈ V ) |
14 |
13
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∈ V ) |
15 |
|
iunexg |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∈ V ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∈ V ) |
16 |
4 14 15
|
syl2anc |
⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∈ V ) |
17 |
6
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐶 𝑋 ∈ 𝐵 ) |
18 |
|
eqid |
⊢ ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) = ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) |
19 |
18
|
fmpox |
⊢ ( ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐶 𝑋 ∈ 𝐵 ↔ ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) : ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ⟶ 𝐵 ) |
20 |
17 19
|
sylib |
⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) : ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ⟶ 𝐵 ) |
21 |
1 2 3 4 5 6 7 8
|
gsum2d2lem |
⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) finSupp 0 ) |
22 |
|
relxp |
⊢ Rel ( { 𝑘 } × 𝐸 ) |
23 |
22
|
rgenw |
⊢ ∀ 𝑘 ∈ 𝐷 Rel ( { 𝑘 } × 𝐸 ) |
24 |
|
reliun |
⊢ ( Rel ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↔ ∀ 𝑘 ∈ 𝐷 Rel ( { 𝑘 } × 𝐸 ) ) |
25 |
23 24
|
mpbir |
⊢ Rel ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) |
26 |
|
cnvf1o |
⊢ ( Rel ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) → ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) : ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto→ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) |
27 |
25 26
|
ax-mp |
⊢ ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) : ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto→ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) |
28 |
|
relxp |
⊢ Rel ( { 𝑗 } × 𝐶 ) |
29 |
28
|
rgenw |
⊢ ∀ 𝑗 ∈ 𝐴 Rel ( { 𝑗 } × 𝐶 ) |
30 |
|
reliun |
⊢ ( Rel ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ ∀ 𝑗 ∈ 𝐴 Rel ( { 𝑗 } × 𝐶 ) ) |
31 |
29 30
|
mpbir |
⊢ Rel ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) |
32 |
|
relcnv |
⊢ Rel ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) |
33 |
|
nfv |
⊢ Ⅎ 𝑘 𝜑 |
34 |
|
nfv |
⊢ Ⅎ 𝑘 〈 𝑥 , 𝑦 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) |
35 |
|
nfiu1 |
⊢ Ⅎ 𝑘 ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) |
36 |
35
|
nfcnv |
⊢ Ⅎ 𝑘 ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) |
37 |
36
|
nfel2 |
⊢ Ⅎ 𝑘 〈 𝑥 , 𝑦 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) |
38 |
34 37
|
nfbi |
⊢ Ⅎ 𝑘 ( 〈 𝑥 , 𝑦 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑦 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) |
39 |
33 38
|
nfim |
⊢ Ⅎ 𝑘 ( 𝜑 → ( 〈 𝑥 , 𝑦 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑦 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) |
40 |
|
opeq2 |
⊢ ( 𝑘 = 𝑦 → 〈 𝑥 , 𝑘 〉 = 〈 𝑥 , 𝑦 〉 ) |
41 |
40
|
eleq1d |
⊢ ( 𝑘 = 𝑦 → ( 〈 𝑥 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑦 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ) ) |
42 |
40
|
eleq1d |
⊢ ( 𝑘 = 𝑦 → ( 〈 𝑥 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↔ 〈 𝑥 , 𝑦 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) |
43 |
41 42
|
bibi12d |
⊢ ( 𝑘 = 𝑦 → ( ( 〈 𝑥 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ↔ ( 〈 𝑥 , 𝑦 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑦 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) ) |
44 |
43
|
imbi2d |
⊢ ( 𝑘 = 𝑦 → ( ( 𝜑 → ( 〈 𝑥 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) ↔ ( 𝜑 → ( 〈 𝑥 , 𝑦 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑦 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) ) ) |
45 |
|
nfv |
⊢ Ⅎ 𝑗 𝜑 |
46 |
|
nfiu1 |
⊢ Ⅎ 𝑗 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) |
47 |
46
|
nfel2 |
⊢ Ⅎ 𝑗 〈 𝑥 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) |
48 |
|
nfv |
⊢ Ⅎ 𝑗 〈 𝑥 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) |
49 |
47 48
|
nfbi |
⊢ Ⅎ 𝑗 ( 〈 𝑥 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) |
50 |
45 49
|
nfim |
⊢ Ⅎ 𝑗 ( 𝜑 → ( 〈 𝑥 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) |
51 |
|
opeq1 |
⊢ ( 𝑗 = 𝑥 → 〈 𝑗 , 𝑘 〉 = 〈 𝑥 , 𝑘 〉 ) |
52 |
51
|
eleq1d |
⊢ ( 𝑗 = 𝑥 → ( 〈 𝑗 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ) ) |
53 |
51
|
eleq1d |
⊢ ( 𝑗 = 𝑥 → ( 〈 𝑗 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↔ 〈 𝑥 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) |
54 |
52 53
|
bibi12d |
⊢ ( 𝑗 = 𝑥 → ( ( 〈 𝑗 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑗 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ↔ ( 〈 𝑥 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) ) |
55 |
54
|
imbi2d |
⊢ ( 𝑗 = 𝑥 → ( ( 𝜑 → ( 〈 𝑗 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑗 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) ↔ ( 𝜑 → ( 〈 𝑥 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) ) ) |
56 |
|
opeliunxp |
⊢ ( 〈 𝑗 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) |
57 |
|
opeliunxp |
⊢ ( 〈 𝑘 , 𝑗 〉 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↔ ( 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸 ) ) |
58 |
10 56 57
|
3bitr4g |
⊢ ( 𝜑 → ( 〈 𝑗 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑘 , 𝑗 〉 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) |
59 |
|
vex |
⊢ 𝑗 ∈ V |
60 |
|
vex |
⊢ 𝑘 ∈ V |
61 |
59 60
|
opelcnv |
⊢ ( 〈 𝑗 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↔ 〈 𝑘 , 𝑗 〉 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) |
62 |
58 61
|
bitr4di |
⊢ ( 𝜑 → ( 〈 𝑗 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑗 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) |
63 |
50 55 62
|
chvarfv |
⊢ ( 𝜑 → ( 〈 𝑥 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑘 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) |
64 |
39 44 63
|
chvarfv |
⊢ ( 𝜑 → ( 〈 𝑥 , 𝑦 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ 〈 𝑥 , 𝑦 〉 ∈ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) |
65 |
31 32 64
|
eqrelrdv |
⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) = ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) |
66 |
65
|
f1oeq3d |
⊢ ( 𝜑 → ( ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) : ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) : ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto→ ◡ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ) ) |
67 |
27 66
|
mpbiri |
⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) : ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ) |
68 |
1 2 3 16 20 21 67
|
gsumf1o |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) = ( 𝐺 Σg ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ∘ ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) ) ) ) |
69 |
|
sneq |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → { 𝑧 } = { 〈 𝑥 , 𝑦 〉 } ) |
70 |
69
|
cnveqd |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ◡ { 𝑧 } = ◡ { 〈 𝑥 , 𝑦 〉 } ) |
71 |
70
|
unieqd |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ∪ ◡ { 𝑧 } = ∪ ◡ { 〈 𝑥 , 𝑦 〉 } ) |
72 |
|
opswap |
⊢ ∪ ◡ { 〈 𝑥 , 𝑦 〉 } = 〈 𝑦 , 𝑥 〉 |
73 |
71 72
|
eqtrdi |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ∪ ◡ { 𝑧 } = 〈 𝑦 , 𝑥 〉 ) |
74 |
73
|
fveq2d |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ ∪ ◡ { 𝑧 } ) = ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 〈 𝑦 , 𝑥 〉 ) ) |
75 |
|
df-ov |
⊢ ( 𝑦 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑥 ) = ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 〈 𝑦 , 𝑥 〉 ) |
76 |
74 75
|
eqtr4di |
⊢ ( 𝑧 = 〈 𝑥 , 𝑦 〉 → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ ∪ ◡ { 𝑧 } ) = ( 𝑦 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑥 ) ) |
77 |
76
|
mpomptx |
⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐷 ( { 𝑥 } × ⦋ 𝑥 / 𝑘 ⦌ 𝐸 ) ↦ ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ ∪ ◡ { 𝑧 } ) ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ⦋ 𝑥 / 𝑘 ⦌ 𝐸 ↦ ( 𝑦 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑥 ) ) |
78 |
|
nfcv |
⊢ Ⅎ 𝑥 ( { 𝑘 } × 𝐸 ) |
79 |
|
nfcv |
⊢ Ⅎ 𝑘 { 𝑥 } |
80 |
|
nfcsb1v |
⊢ Ⅎ 𝑘 ⦋ 𝑥 / 𝑘 ⦌ 𝐸 |
81 |
79 80
|
nfxp |
⊢ Ⅎ 𝑘 ( { 𝑥 } × ⦋ 𝑥 / 𝑘 ⦌ 𝐸 ) |
82 |
|
sneq |
⊢ ( 𝑘 = 𝑥 → { 𝑘 } = { 𝑥 } ) |
83 |
|
csbeq1a |
⊢ ( 𝑘 = 𝑥 → 𝐸 = ⦋ 𝑥 / 𝑘 ⦌ 𝐸 ) |
84 |
82 83
|
xpeq12d |
⊢ ( 𝑘 = 𝑥 → ( { 𝑘 } × 𝐸 ) = ( { 𝑥 } × ⦋ 𝑥 / 𝑘 ⦌ 𝐸 ) ) |
85 |
78 81 84
|
cbviun |
⊢ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) = ∪ 𝑥 ∈ 𝐷 ( { 𝑥 } × ⦋ 𝑥 / 𝑘 ⦌ 𝐸 ) |
86 |
85
|
mpteq1i |
⊢ ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ ∪ ◡ { 𝑧 } ) ) = ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐷 ( { 𝑥 } × ⦋ 𝑥 / 𝑘 ⦌ 𝐸 ) ↦ ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ ∪ ◡ { 𝑧 } ) ) |
87 |
|
nfcv |
⊢ Ⅎ 𝑥 𝐸 |
88 |
|
nfcv |
⊢ Ⅎ 𝑥 ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) |
89 |
|
nfcv |
⊢ Ⅎ 𝑦 ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) |
90 |
|
nfcv |
⊢ Ⅎ 𝑘 𝑦 |
91 |
|
nfmpo2 |
⊢ Ⅎ 𝑘 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) |
92 |
|
nfcv |
⊢ Ⅎ 𝑘 𝑥 |
93 |
90 91 92
|
nfov |
⊢ Ⅎ 𝑘 ( 𝑦 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑥 ) |
94 |
|
nfcv |
⊢ Ⅎ 𝑗 𝑦 |
95 |
|
nfmpo1 |
⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) |
96 |
|
nfcv |
⊢ Ⅎ 𝑗 𝑥 |
97 |
94 95 96
|
nfov |
⊢ Ⅎ 𝑗 ( 𝑦 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑥 ) |
98 |
|
oveq2 |
⊢ ( 𝑘 = 𝑥 → ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) = ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑥 ) ) |
99 |
|
oveq1 |
⊢ ( 𝑗 = 𝑦 → ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑥 ) = ( 𝑦 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑥 ) ) |
100 |
98 99
|
sylan9eq |
⊢ ( ( 𝑘 = 𝑥 ∧ 𝑗 = 𝑦 ) → ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) = ( 𝑦 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑥 ) ) |
101 |
87 80 88 89 93 97 83 100
|
cbvmpox |
⊢ ( 𝑘 ∈ 𝐷 , 𝑗 ∈ 𝐸 ↦ ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) ) = ( 𝑥 ∈ 𝐷 , 𝑦 ∈ ⦋ 𝑥 / 𝑘 ⦌ 𝐸 ↦ ( 𝑦 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑥 ) ) |
102 |
77 86 101
|
3eqtr4i |
⊢ ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ ∪ ◡ { 𝑧 } ) ) = ( 𝑘 ∈ 𝐷 , 𝑗 ∈ 𝐸 ↦ ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) ) |
103 |
|
f1of |
⊢ ( ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) : ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) –1-1-onto→ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) → ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) : ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ⟶ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ) |
104 |
67 103
|
syl |
⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) : ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ⟶ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ) |
105 |
|
eqid |
⊢ ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) = ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) |
106 |
105
|
fmpt |
⊢ ( ∀ 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ∪ ◡ { 𝑧 } ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) : ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ⟶ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ) |
107 |
104 106
|
sylibr |
⊢ ( 𝜑 → ∀ 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ∪ ◡ { 𝑧 } ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ) |
108 |
|
eqidd |
⊢ ( 𝜑 → ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) = ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) ) |
109 |
20
|
feqmptd |
⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) = ( 𝑥 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↦ ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 𝑥 ) ) ) |
110 |
|
fveq2 |
⊢ ( 𝑥 = ∪ ◡ { 𝑧 } → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 𝑥 ) = ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ ∪ ◡ { 𝑧 } ) ) |
111 |
107 108 109 110
|
fmptcof |
⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ∘ ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) ) = ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ ∪ ◡ { 𝑧 } ) ) ) |
112 |
6
|
ex |
⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) → 𝑋 ∈ 𝐵 ) ) |
113 |
18
|
ovmpt4g |
⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) = 𝑋 ) |
114 |
113
|
3expia |
⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) → ( 𝑋 ∈ 𝐵 → ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) = 𝑋 ) ) |
115 |
112 114
|
sylcom |
⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) → ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) = 𝑋 ) ) |
116 |
10 115
|
sylbird |
⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸 ) → ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) = 𝑋 ) ) |
117 |
116
|
3impib |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸 ) → ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) = 𝑋 ) |
118 |
117
|
eqcomd |
⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐷 ∧ 𝑗 ∈ 𝐸 ) → 𝑋 = ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) ) |
119 |
118
|
mpoeq3dva |
⊢ ( 𝜑 → ( 𝑘 ∈ 𝐷 , 𝑗 ∈ 𝐸 ↦ 𝑋 ) = ( 𝑘 ∈ 𝐷 , 𝑗 ∈ 𝐸 ↦ ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) ) ) |
120 |
102 111 119
|
3eqtr4a |
⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ∘ ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) ) = ( 𝑘 ∈ 𝐷 , 𝑗 ∈ 𝐸 ↦ 𝑋 ) ) |
121 |
120
|
oveq2d |
⊢ ( 𝜑 → ( 𝐺 Σg ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ∘ ( 𝑧 ∈ ∪ 𝑘 ∈ 𝐷 ( { 𝑘 } × 𝐸 ) ↦ ∪ ◡ { 𝑧 } ) ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐷 , 𝑗 ∈ 𝐸 ↦ 𝑋 ) ) ) |
122 |
68 121
|
eqtrd |
⊢ ( 𝜑 → ( 𝐺 Σg ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) = ( 𝐺 Σg ( 𝑘 ∈ 𝐷 , 𝑗 ∈ 𝐸 ↦ 𝑋 ) ) ) |