| Step | Hyp | Ref
| Expression |
| 1 | | gsum2d2.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
| 2 | | gsum2d2.z |
. . 3
⊢ 0 =
(0g‘𝐺) |
| 3 | | gsum2d2.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ CMnd) |
| 4 | | gsum2d2.a |
. . . 4
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
| 5 | | vsnex 5434 |
. . . . . 6
⊢ {𝑗} ∈ V |
| 6 | | gsum2d2.r |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐶 ∈ 𝑊) |
| 7 | | xpexg 7770 |
. . . . . 6
⊢ (({𝑗} ∈ V ∧ 𝐶 ∈ 𝑊) → ({𝑗} × 𝐶) ∈ V) |
| 8 | 5, 6, 7 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ({𝑗} × 𝐶) ∈ V) |
| 9 | 8 | ralrimiva 3146 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
| 10 | | iunexg 7988 |
. . . 4
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
| 11 | 4, 9, 10 | syl2anc 584 |
. . 3
⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ∈ V) |
| 12 | | relxp 5703 |
. . . . . 6
⊢ Rel
({𝑗} × 𝐶) |
| 13 | 12 | rgenw 3065 |
. . . . 5
⊢
∀𝑗 ∈
𝐴 Rel ({𝑗} × 𝐶) |
| 14 | | reliun 5826 |
. . . . 5
⊢ (Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ ∀𝑗 ∈ 𝐴 Rel ({𝑗} × 𝐶)) |
| 15 | 13, 14 | mpbir 231 |
. . . 4
⊢ Rel
∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
| 16 | 15 | a1i 11 |
. . 3
⊢ (𝜑 → Rel ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
| 17 | | vex 3484 |
. . . . . 6
⊢ 𝑥 ∈ V |
| 18 | 17 | eldm2 5912 |
. . . . 5
⊢ (𝑥 ∈ dom ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ ∃𝑦〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
| 19 | | eliunxp 5848 |
. . . . . . 7
⊢
(〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ ∃𝑗∃𝑘(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶))) |
| 20 | | vex 3484 |
. . . . . . . . . . . 12
⊢ 𝑦 ∈ V |
| 21 | 17, 20 | opth1 5480 |
. . . . . . . . . . 11
⊢
(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 → 𝑥 = 𝑗) |
| 22 | 21 | ad2antrl 728 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶))) → 𝑥 = 𝑗) |
| 23 | | simprrl 781 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶))) → 𝑗 ∈ 𝐴) |
| 24 | 22, 23 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶))) → 𝑥 ∈ 𝐴) |
| 25 | 24 | ex 412 |
. . . . . . . 8
⊢ (𝜑 → ((〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑥 ∈ 𝐴)) |
| 26 | 25 | exlimdvv 1934 |
. . . . . . 7
⊢ (𝜑 → (∃𝑗∃𝑘(〈𝑥, 𝑦〉 = 〈𝑗, 𝑘〉 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑥 ∈ 𝐴)) |
| 27 | 19, 26 | biimtrid 242 |
. . . . . 6
⊢ (𝜑 → (〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) → 𝑥 ∈ 𝐴)) |
| 28 | 27 | exlimdv 1933 |
. . . . 5
⊢ (𝜑 → (∃𝑦〈𝑥, 𝑦〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) → 𝑥 ∈ 𝐴)) |
| 29 | 18, 28 | biimtrid 242 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ dom ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) → 𝑥 ∈ 𝐴)) |
| 30 | 29 | ssrdv 3989 |
. . 3
⊢ (𝜑 → dom ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ⊆ 𝐴) |
| 31 | | gsum2d2.f |
. . . . 5
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑋 ∈ 𝐵) |
| 32 | 31 | ralrimivva 3202 |
. . . 4
⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵) |
| 33 | | eqid 2737 |
. . . . 5
⊢ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) = (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
| 34 | 33 | fmpox 8092 |
. . . 4
⊢
(∀𝑗 ∈
𝐴 ∀𝑘 ∈ 𝐶 𝑋 ∈ 𝐵 ↔ (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
| 35 | 32, 34 | sylib 218 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋):∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)⟶𝐵) |
| 36 | | gsum2d2.u |
. . . 4
⊢ (𝜑 → 𝑈 ∈ Fin) |
| 37 | | gsum2d2.n |
. . . 4
⊢ ((𝜑 ∧ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶) ∧ ¬ 𝑗𝑈𝑘)) → 𝑋 = 0 ) |
| 38 | 1, 2, 3, 4, 6, 31,
36, 37 | gsum2d2lem 19991 |
. . 3
⊢ (𝜑 → (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) finSupp 0 ) |
| 39 | 1, 2, 3, 11, 16, 4, 30, 35, 38 | gsum2d 19990 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑚 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))))) |
| 40 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑗𝐺 |
| 41 | | nfcv 2905 |
. . . . . 6
⊢
Ⅎ𝑗
Σg |
| 42 | | nfiu1 5027 |
. . . . . . . 8
⊢
Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) |
| 43 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑗{𝑚} |
| 44 | 42, 43 | nfima 6086 |
. . . . . . 7
⊢
Ⅎ𝑗(∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) |
| 45 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑗𝑚 |
| 46 | | nfmpo1 7513 |
. . . . . . . 8
⊢
Ⅎ𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
| 47 | | nfcv 2905 |
. . . . . . . 8
⊢
Ⅎ𝑗𝑛 |
| 48 | 45, 46, 47 | nfov 7461 |
. . . . . . 7
⊢
Ⅎ𝑗(𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛) |
| 49 | 44, 48 | nfmpt 5249 |
. . . . . 6
⊢
Ⅎ𝑗(𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) |
| 50 | 40, 41, 49 | nfov 7461 |
. . . . 5
⊢
Ⅎ𝑗(𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) |
| 51 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑚(𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) |
| 52 | | sneq 4636 |
. . . . . . . 8
⊢ (𝑚 = 𝑗 → {𝑚} = {𝑗}) |
| 53 | 52 | imaeq2d 6078 |
. . . . . . 7
⊢ (𝑚 = 𝑗 → (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) = (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗})) |
| 54 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑚 = 𝑗 → (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛) = (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) |
| 55 | 53, 54 | mpteq12dv 5233 |
. . . . . 6
⊢ (𝑚 = 𝑗 → (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) |
| 56 | 55 | oveq2d 7447 |
. . . . 5
⊢ (𝑚 = 𝑗 → (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) = (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))) |
| 57 | 50, 51, 56 | cbvmpt 5253 |
. . . 4
⊢ (𝑚 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))) = (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))) |
| 58 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑗 ∈ V |
| 59 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑘 ∈ V |
| 60 | 58, 59 | elimasn 6108 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↔ 〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶)) |
| 61 | | opeliunxp 5752 |
. . . . . . . . . . . . 13
⊢
(〈𝑗, 𝑘〉 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) ↔ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) |
| 62 | 60, 61 | bitri 275 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↔ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) |
| 63 | 62 | baib 535 |
. . . . . . . . . . 11
⊢ (𝑗 ∈ 𝐴 → (𝑘 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↔ 𝑘 ∈ 𝐶)) |
| 64 | 63 | eqrdv 2735 |
. . . . . . . . . 10
⊢ (𝑗 ∈ 𝐴 → (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) = 𝐶) |
| 65 | 64 | mpteq1d 5237 |
. . . . . . . . 9
⊢ (𝑗 ∈ 𝐴 → (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑛 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) |
| 66 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘𝑗 |
| 67 | | nfmpo2 7514 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋) |
| 68 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑘𝑛 |
| 69 | 66, 67, 68 | nfov 7461 |
. . . . . . . . . 10
⊢
Ⅎ𝑘(𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛) |
| 70 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑛(𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) |
| 71 | | oveq2 7439 |
. . . . . . . . . 10
⊢ (𝑛 = 𝑘 → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛) = (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) |
| 72 | 69, 70, 71 | cbvmpt 5253 |
. . . . . . . . 9
⊢ (𝑛 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑘 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) |
| 73 | 65, 72 | eqtrdi 2793 |
. . . . . . . 8
⊢ (𝑗 ∈ 𝐴 → (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑘 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘))) |
| 74 | 73 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑘 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘))) |
| 75 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑗 ∈ 𝐴) |
| 76 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → 𝑘 ∈ 𝐶) |
| 77 | 33 | ovmpt4g 7580 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
| 78 | 75, 76, 31, 77 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶)) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
| 79 | 78 | anassrs 467 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐶) → (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘) = 𝑋) |
| 80 | 79 | mpteq2dva 5242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑘 ∈ 𝐶 ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑘)) = (𝑘 ∈ 𝐶 ↦ 𝑋)) |
| 81 | 74, 80 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝑛 ∈ (∪
𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)) = (𝑘 ∈ 𝐶 ↦ 𝑋)) |
| 82 | 81 | oveq2d 7447 |
. . . . 5
⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))) = (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋))) |
| 83 | 82 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑗}) ↦ (𝑗(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))) = (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)))) |
| 84 | 57, 83 | eqtrid 2789 |
. . 3
⊢ (𝜑 → (𝑚 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛)))) = (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋)))) |
| 85 | 84 | oveq2d 7447 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑚 ∈ 𝐴 ↦ (𝐺 Σg (𝑛 ∈ (∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐶) “ {𝑚}) ↦ (𝑚(𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)𝑛))))) = (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋))))) |
| 86 | 39, 85 | eqtrd 2777 |
1
⊢ (𝜑 → (𝐺 Σg (𝑗 ∈ 𝐴, 𝑘 ∈ 𝐶 ↦ 𝑋)) = (𝐺 Σg (𝑗 ∈ 𝐴 ↦ (𝐺 Σg (𝑘 ∈ 𝐶 ↦ 𝑋))))) |