Step | Hyp | Ref
| Expression |
1 | | gsumpart.b |
. . 3
⊢ 𝐵 = (Base‘𝐺) |
2 | | gsumpart.z |
. . 3
⊢ 0 =
(0g‘𝐺) |
3 | | gsumpart.g |
. . 3
⊢ (𝜑 → 𝐺 ∈ CMnd) |
4 | | gsumpart.a |
. . 3
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
5 | | gsumpart.f |
. . 3
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
6 | | gsumpart.w |
. . 3
⊢ (𝜑 → 𝐹 finSupp 0 ) |
7 | | eqid 2759 |
. . . 4
⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) = ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) |
8 | | gsumpart.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
9 | | gsumpart.1 |
. . . 4
⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) |
10 | | gsumpart.2 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) |
11 | 7, 4, 8, 9, 10 | 2ndresdjuf1o 30495 |
. . 3
⊢ (𝜑 → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)–1-1-onto→𝐴) |
12 | 1, 2, 3, 4, 5, 6, 11 | gsumf1o 19089 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))))) |
13 | | snex 5293 |
. . . . . . 7
⊢ {𝑥} ∈ V |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ V) |
15 | 4 | adantr 485 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑉) |
16 | | ssidd 3911 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ 𝐴) |
17 | 10, 16 | eqsstrd 3926 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴) |
18 | | iunss 4927 |
. . . . . . . . 9
⊢ (∪ 𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴 ↔ ∀𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴) |
19 | 17, 18 | sylib 221 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴) |
20 | 19 | r19.21bi 3135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ⊆ 𝐴) |
21 | 15, 20 | ssexd 5187 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ V) |
22 | 14, 21 | xpexd 7465 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ({𝑥} × 𝐶) ∈ V) |
23 | 22 | ralrimiva 3111 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ∈ V) |
24 | | iunexg 7661 |
. . . 4
⊢ ((𝑋 ∈ 𝑊 ∧ ∀𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ∈ V) → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ∈ V) |
25 | 8, 23, 24 | syl2anc 588 |
. . 3
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ∈ V) |
26 | | relxp 5535 |
. . . . . 6
⊢ Rel
({𝑥} × 𝐶) |
27 | 26 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Rel ({𝑥} × 𝐶)) |
28 | 27 | ralrimiva 3111 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 Rel ({𝑥} × 𝐶)) |
29 | | reliun 5651 |
. . . 4
⊢ (Rel
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∀𝑥 ∈ 𝑋 Rel ({𝑥} × 𝐶)) |
30 | 28, 29 | sylibr 237 |
. . 3
⊢ (𝜑 → Rel ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
31 | | dmiun 5746 |
. . . . . 6
⊢ dom
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) = ∪
𝑥 ∈ 𝑋 dom ({𝑥} × 𝐶) |
32 | | dmxpss 5993 |
. . . . . . . 8
⊢ dom
({𝑥} × 𝐶) ⊆ {𝑥} |
33 | 32 | rgenw 3080 |
. . . . . . 7
⊢
∀𝑥 ∈
𝑋 dom ({𝑥} × 𝐶) ⊆ {𝑥} |
34 | | ss2iun 4894 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑋 dom ({𝑥} × 𝐶) ⊆ {𝑥} → ∪
𝑥 ∈ 𝑋 dom ({𝑥} × 𝐶) ⊆ ∪ 𝑥 ∈ 𝑋 {𝑥}) |
35 | 33, 34 | ax-mp 5 |
. . . . . 6
⊢ ∪ 𝑥 ∈ 𝑋 dom ({𝑥} × 𝐶) ⊆ ∪ 𝑥 ∈ 𝑋 {𝑥} |
36 | 31, 35 | eqsstri 3922 |
. . . . 5
⊢ dom
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ ∪ 𝑥 ∈ 𝑋 {𝑥} |
37 | | iunid 4942 |
. . . . 5
⊢ ∪ 𝑥 ∈ 𝑋 {𝑥} = 𝑋 |
38 | 36, 37 | sseqtri 3924 |
. . . 4
⊢ dom
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ 𝑋 |
39 | 38 | a1i 11 |
. . 3
⊢ (𝜑 → dom ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ 𝑋) |
40 | | fo2nd 7707 |
. . . . . . . 8
⊢
2nd :V–onto→V |
41 | | fof 6569 |
. . . . . . . 8
⊢
(2nd :V–onto→V → 2nd
:V⟶V) |
42 | 40, 41 | ax-mp 5 |
. . . . . . 7
⊢
2nd :V⟶V |
43 | | ssv 3912 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ V |
44 | | fssres 6522 |
. . . . . . 7
⊢
((2nd :V⟶V ∧ ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ V) → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶V) |
45 | 42, 43, 44 | mp2an 692 |
. . . . . 6
⊢
(2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶V |
46 | | ffn 6491 |
. . . . . 6
⊢
((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶V → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) Fn ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
47 | 45, 46 | mp1i 13 |
. . . . 5
⊢ (𝜑 → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) Fn ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
48 | | djussxp2 30493 |
. . . . . . . 8
⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × ∪
𝑥 ∈ 𝑋 𝐶) |
49 | | imass2 5930 |
. . . . . . . 8
⊢ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × ∪
𝑥 ∈ 𝑋 𝐶) → (2nd “ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ (2nd “ (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶))) |
50 | 48, 49 | ax-mp 5 |
. . . . . . 7
⊢
(2nd “ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ (2nd “ (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)) |
51 | | ima0 5910 |
. . . . . . . . . . 11
⊢
(2nd “ ∅) = ∅ |
52 | | xpeq1 5531 |
. . . . . . . . . . . . 13
⊢ (𝑋 = ∅ → (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶) = (∅ × ∪ 𝑥 ∈ 𝑋 𝐶)) |
53 | | 0xp 5611 |
. . . . . . . . . . . . 13
⊢ (∅
× ∪ 𝑥 ∈ 𝑋 𝐶) = ∅ |
54 | 52, 53 | eqtrdi 2810 |
. . . . . . . . . . . 12
⊢ (𝑋 = ∅ → (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶) = ∅) |
55 | 54 | imaeq2d 5894 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ →
(2nd “ (𝑋
× ∪ 𝑥 ∈ 𝑋 𝐶)) = (2nd “
∅)) |
56 | | iuneq1 4892 |
. . . . . . . . . . . 12
⊢ (𝑋 = ∅ → ∪ 𝑥 ∈ 𝑋 𝐶 = ∪ 𝑥 ∈ ∅ 𝐶) |
57 | | 0iun 4944 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 ∈ ∅ 𝐶 = ∅ |
58 | 56, 57 | eqtrdi 2810 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → ∪ 𝑥 ∈ 𝑋 𝐶 = ∅) |
59 | 51, 55, 58 | 3eqtr4a 2820 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ →
(2nd “ (𝑋
× ∪ 𝑥 ∈ 𝑋 𝐶)) = ∪
𝑥 ∈ 𝑋 𝐶) |
60 | 59 | adantl 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → (2nd “
(𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)) = ∪
𝑥 ∈ 𝑋 𝐶) |
61 | | 2ndimaxp 30492 |
. . . . . . . . . 10
⊢ (𝑋 ≠ ∅ →
(2nd “ (𝑋
× ∪ 𝑥 ∈ 𝑋 𝐶)) = ∪
𝑥 ∈ 𝑋 𝐶) |
62 | 61 | adantl 486 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (2nd
“ (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)) = ∪
𝑥 ∈ 𝑋 𝐶) |
63 | 60, 62 | pm2.61dane 3036 |
. . . . . . . 8
⊢ (𝜑 → (2nd “
(𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)) = ∪
𝑥 ∈ 𝑋 𝐶) |
64 | 63, 10 | eqtrd 2794 |
. . . . . . 7
⊢ (𝜑 → (2nd “
(𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)) = 𝐴) |
65 | 50, 64 | sseqtrid 3940 |
. . . . . 6
⊢ (𝜑 → (2nd “
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ 𝐴) |
66 | | resssxp 6092 |
. . . . . 6
⊢
((2nd “ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ 𝐴 ↔ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) × 𝐴)) |
67 | 65, 66 | sylib 221 |
. . . . 5
⊢ (𝜑 → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) × 𝐴)) |
68 | | dff2 6849 |
. . . . 5
⊢
((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶𝐴 ↔ ((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) Fn ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ∧ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) × 𝐴))) |
69 | 47, 67, 68 | sylanbrc 587 |
. . . 4
⊢ (𝜑 → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶𝐴) |
70 | 5, 69 | fcod 6510 |
. . 3
⊢ (𝜑 → (𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))):∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶𝐵) |
71 | 7, 4, 8, 9, 10 | 2ndresdju 30494 |
. . . 4
⊢ (𝜑 → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)–1-1→𝐴) |
72 | 2 | fvexi 6665 |
. . . . 5
⊢ 0 ∈
V |
73 | 72 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈ V) |
74 | 5, 4 | fexd 6974 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ V) |
75 | 6, 71, 73, 74 | fsuppco 8884 |
. . 3
⊢ (𝜑 → (𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))) finSupp 0 ) |
76 | 1, 2, 3, 25, 30, 8, 39, 70, 75 | gsum2d 19145 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘ (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))) = (𝐺 Σg (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝑧 ∈ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧)))))) |
77 | | nfcsb1v 3825 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶 |
78 | | csbeq1a 3815 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶) |
79 | 8, 21, 77, 78 | iunsnima2 30466 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) = ⦋𝑦 / 𝑥⦌𝐶) |
80 | | df-ov 7146 |
. . . . . . . . 9
⊢ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧) = ((𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))‘〈𝑦, 𝑧〉) |
81 | 69 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶𝐴) |
82 | | simplr 769 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → 𝑦 ∈ 𝑋) |
83 | | vsnid 4552 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ {𝑦} |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → 𝑦 ∈ {𝑦}) |
85 | 79 | eleq2d 2836 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↔ 𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
86 | 85 | biimpa 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → 𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐶) |
87 | 84, 86 | opelxpd 5555 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → 〈𝑦, 𝑧〉 ∈ ({𝑦} × ⦋𝑦 / 𝑥⦌𝐶)) |
88 | | nfcv 2917 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥{𝑦} |
89 | 88, 77 | nfxp 5550 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥({𝑦} × ⦋𝑦 / 𝑥⦌𝐶) |
90 | 89 | nfel2 2935 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥〈𝑦, 𝑧〉 ∈ ({𝑦} × ⦋𝑦 / 𝑥⦌𝐶) |
91 | | sneq 4525 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
92 | 91, 78 | xpeq12d 5548 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ({𝑥} × 𝐶) = ({𝑦} × ⦋𝑦 / 𝑥⦌𝐶)) |
93 | 92 | eleq2d 2836 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (〈𝑦, 𝑧〉 ∈ ({𝑥} × 𝐶) ↔ 〈𝑦, 𝑧〉 ∈ ({𝑦} × ⦋𝑦 / 𝑥⦌𝐶))) |
94 | 90, 93 | rspce 3528 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑋 ∧ 〈𝑦, 𝑧〉 ∈ ({𝑦} × ⦋𝑦 / 𝑥⦌𝐶)) → ∃𝑥 ∈ 𝑋 〈𝑦, 𝑧〉 ∈ ({𝑥} × 𝐶)) |
95 | 82, 87, 94 | syl2anc 588 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ∃𝑥 ∈ 𝑋 〈𝑦, 𝑧〉 ∈ ({𝑥} × 𝐶)) |
96 | | eliun 4880 |
. . . . . . . . . . . 12
⊢
(〈𝑦, 𝑧〉 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥 ∈ 𝑋 〈𝑦, 𝑧〉 ∈ ({𝑥} × 𝐶)) |
97 | 95, 96 | sylibr 237 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → 〈𝑦, 𝑧〉 ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
98 | 81, 97 | fvco3d 6745 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))‘〈𝑦, 𝑧〉) = (𝐹‘((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))‘〈𝑦, 𝑧〉))) |
99 | 97 | fvresd 6671 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))‘〈𝑦, 𝑧〉) = (2nd ‘〈𝑦, 𝑧〉)) |
100 | | vex 3411 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
101 | | vex 3411 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
102 | 100, 101 | op2nd 7695 |
. . . . . . . . . . . 12
⊢
(2nd ‘〈𝑦, 𝑧〉) = 𝑧 |
103 | 99, 102 | eqtrdi 2810 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))‘〈𝑦, 𝑧〉) = 𝑧) |
104 | 103 | fveq2d 6655 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → (𝐹‘((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))‘〈𝑦, 𝑧〉)) = (𝐹‘𝑧)) |
105 | 98, 104 | eqtrd 2794 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))‘〈𝑦, 𝑧〉) = (𝐹‘𝑧)) |
106 | 80, 105 | syl5eq 2806 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧) = (𝐹‘𝑧)) |
107 | 79, 106 | mpteq12dva 5109 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧)) = (𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐶 ↦ (𝐹‘𝑧))) |
108 | 5 | adantr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐹:𝐴⟶𝐵) |
109 | | imassrn 5905 |
. . . . . . . . . 10
⊢ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ⊆ ran ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) |
110 | 10 | xpeq2d 5547 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 × ∪
𝑥 ∈ 𝑋 𝐶) = (𝑋 × 𝐴)) |
111 | 48, 110 | sseqtrid 3940 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴)) |
112 | | rnss 5773 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴) → ran ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ ran (𝑋 × 𝐴)) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ ran (𝑋 × 𝐴)) |
114 | 113 | adantr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ran ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ ran (𝑋 × 𝐴)) |
115 | | rnxpss 5994 |
. . . . . . . . . . 11
⊢ ran
(𝑋 × 𝐴) ⊆ 𝐴 |
116 | 114, 115 | sstrdi 3900 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ran ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ 𝐴) |
117 | 109, 116 | sstrid 3899 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ⊆ 𝐴) |
118 | 79, 117 | eqsstrrd 3927 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ⦋𝑦 / 𝑥⦌𝐶 ⊆ 𝐴) |
119 | 108, 118 | feqresmpt 6715 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶) = (𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐶 ↦ (𝐹‘𝑧))) |
120 | 107, 119 | eqtr4d 2797 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧)) = (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶)) |
121 | 120 | oveq2d 7159 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐺 Σg (𝑧 ∈ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧))) = (𝐺 Σg (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶))) |
122 | 121 | mpteq2dva 5120 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝑧 ∈ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧)))) = (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶)))) |
123 | | nfcv 2917 |
. . . . 5
⊢
Ⅎ𝑦(𝐺 Σg (𝐹 ↾ 𝐶)) |
124 | | nfcv 2917 |
. . . . . 6
⊢
Ⅎ𝑥𝐺 |
125 | | nfcv 2917 |
. . . . . 6
⊢
Ⅎ𝑥
Σg |
126 | | nfcv 2917 |
. . . . . . 7
⊢
Ⅎ𝑥𝐹 |
127 | 126, 77 | nfres 5818 |
. . . . . 6
⊢
Ⅎ𝑥(𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶) |
128 | 124, 125,
127 | nfov 7173 |
. . . . 5
⊢
Ⅎ𝑥(𝐺 Σg (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶)) |
129 | 78 | reseq2d 5816 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐹 ↾ 𝐶) = (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶)) |
130 | 129 | oveq2d 7159 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝐹 ↾ 𝐶)) = (𝐺 Σg (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶))) |
131 | 123, 128,
130 | cbvmpt 5126 |
. . . 4
⊢ (𝑥 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ 𝐶))) = (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶))) |
132 | 122, 131 | eqtr4di 2812 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝑧 ∈ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧)))) = (𝑥 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ 𝐶)))) |
133 | 132 | oveq2d 7159 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝑧 ∈ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧))))) = (𝐺 Σg (𝑥 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ 𝐶))))) |
134 | 12, 76, 133 | 3eqtrd 2798 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ 𝐶))))) |