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 2733 |
. . . 4
⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) = ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) |
8 | | gsumpart.x |
. . . 4
⊢ (𝜑 → 𝑋 ∈ 𝑊) |
9 | | gsumpart.1 |
. . . 4
⊢ (𝜑 → Disj 𝑥 ∈ 𝑋 𝐶) |
10 | | gsumpart.2 |
. . . 4
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴) |
11 | 7, 4, 8, 9, 10 | 2ndresdjuf1o 31612 |
. . 3
⊢ (𝜑 → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)–1-1-onto→𝐴) |
12 | 1, 2, 3, 4, 5, 6, 11 | gsumf1o 19698 |
. 2
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝐹 ∘ (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))))) |
13 | | vsnex 5387 |
. . . . . . 7
⊢ {𝑥} ∈ V |
14 | 13 | a1i 11 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → {𝑥} ∈ V) |
15 | 4 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐴 ∈ 𝑉) |
16 | | ssidd 3968 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ⊆ 𝐴) |
17 | 10, 16 | eqsstrd 3983 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴) |
18 | | iunss 5006 |
. . . . . . . . 9
⊢ (∪ 𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴 ↔ ∀𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴) |
19 | 17, 18 | sylib 217 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 𝐶 ⊆ 𝐴) |
20 | 19 | r19.21bi 3233 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ⊆ 𝐴) |
21 | 15, 20 | ssexd 5282 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → 𝐶 ∈ V) |
22 | 14, 21 | xpexd 7686 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → ({𝑥} × 𝐶) ∈ V) |
23 | 22 | ralrimiva 3140 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ∈ V) |
24 | | iunexg 7897 |
. . . 4
⊢ ((𝑋 ∈ 𝑊 ∧ ∀𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ∈ V) → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ∈ V) |
25 | 8, 23, 24 | syl2anc 585 |
. . 3
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ∈ V) |
26 | | relxp 5652 |
. . . . . 6
⊢ Rel
({𝑥} × 𝐶) |
27 | 26 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → Rel ({𝑥} × 𝐶)) |
28 | 27 | ralrimiva 3140 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝑋 Rel ({𝑥} × 𝐶)) |
29 | | reliun 5773 |
. . . 4
⊢ (Rel
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∀𝑥 ∈ 𝑋 Rel ({𝑥} × 𝐶)) |
30 | 28, 29 | sylibr 233 |
. . 3
⊢ (𝜑 → Rel ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
31 | | dmiun 5870 |
. . . . . 6
⊢ dom
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) = ∪
𝑥 ∈ 𝑋 dom ({𝑥} × 𝐶) |
32 | | dmxpss 6124 |
. . . . . . . 8
⊢ dom
({𝑥} × 𝐶) ⊆ {𝑥} |
33 | 32 | rgenw 3065 |
. . . . . . 7
⊢
∀𝑥 ∈
𝑋 dom ({𝑥} × 𝐶) ⊆ {𝑥} |
34 | | ss2iun 4973 |
. . . . . . 7
⊢
(∀𝑥 ∈
𝑋 dom ({𝑥} × 𝐶) ⊆ {𝑥} → ∪
𝑥 ∈ 𝑋 dom ({𝑥} × 𝐶) ⊆ ∪ 𝑥 ∈ 𝑋 {𝑥}) |
35 | 33, 34 | ax-mp 5 |
. . . . . 6
⊢ ∪ 𝑥 ∈ 𝑋 dom ({𝑥} × 𝐶) ⊆ ∪ 𝑥 ∈ 𝑋 {𝑥} |
36 | 31, 35 | eqsstri 3979 |
. . . . 5
⊢ dom
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ ∪ 𝑥 ∈ 𝑋 {𝑥} |
37 | | iunid 5021 |
. . . . 5
⊢ ∪ 𝑥 ∈ 𝑋 {𝑥} = 𝑋 |
38 | 36, 37 | sseqtri 3981 |
. . . 4
⊢ dom
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ 𝑋 |
39 | 38 | a1i 11 |
. . 3
⊢ (𝜑 → dom ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ 𝑋) |
40 | | fo2nd 7943 |
. . . . . . . 8
⊢
2nd :V–onto→V |
41 | | fof 6757 |
. . . . . . . 8
⊢
(2nd :V–onto→V → 2nd
:V⟶V) |
42 | 40, 41 | ax-mp 5 |
. . . . . . 7
⊢
2nd :V⟶V |
43 | | ssv 3969 |
. . . . . . 7
⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ V |
44 | | fssres 6709 |
. . . . . . 7
⊢
((2nd :V⟶V ∧ ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ V) → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶V) |
45 | 42, 43, 44 | mp2an 691 |
. . . . . 6
⊢
(2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶V |
46 | | ffn 6669 |
. . . . . 6
⊢
((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶V → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) Fn ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
47 | 45, 46 | mp1i 13 |
. . . . 5
⊢ (𝜑 → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) Fn ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
48 | | djussxp2 31610 |
. . . . . . . 8
⊢ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × ∪
𝑥 ∈ 𝑋 𝐶) |
49 | | imass2 6055 |
. . . . . . . 8
⊢ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × ∪
𝑥 ∈ 𝑋 𝐶) → (2nd “ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ (2nd “ (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶))) |
50 | 48, 49 | ax-mp 5 |
. . . . . . 7
⊢
(2nd “ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ (2nd “ (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)) |
51 | | ima0 6030 |
. . . . . . . . . . 11
⊢
(2nd “ ∅) = ∅ |
52 | | xpeq1 5648 |
. . . . . . . . . . . . 13
⊢ (𝑋 = ∅ → (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶) = (∅ × ∪ 𝑥 ∈ 𝑋 𝐶)) |
53 | | 0xp 5731 |
. . . . . . . . . . . . 13
⊢ (∅
× ∪ 𝑥 ∈ 𝑋 𝐶) = ∅ |
54 | 52, 53 | eqtrdi 2789 |
. . . . . . . . . . . 12
⊢ (𝑋 = ∅ → (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶) = ∅) |
55 | 54 | imaeq2d 6014 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ →
(2nd “ (𝑋
× ∪ 𝑥 ∈ 𝑋 𝐶)) = (2nd “
∅)) |
56 | | iuneq1 4971 |
. . . . . . . . . . . 12
⊢ (𝑋 = ∅ → ∪ 𝑥 ∈ 𝑋 𝐶 = ∪ 𝑥 ∈ ∅ 𝐶) |
57 | | 0iun 5024 |
. . . . . . . . . . . 12
⊢ ∪ 𝑥 ∈ ∅ 𝐶 = ∅ |
58 | 56, 57 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ (𝑋 = ∅ → ∪ 𝑥 ∈ 𝑋 𝐶 = ∅) |
59 | 51, 55, 58 | 3eqtr4a 2799 |
. . . . . . . . . 10
⊢ (𝑋 = ∅ →
(2nd “ (𝑋
× ∪ 𝑥 ∈ 𝑋 𝐶)) = ∪
𝑥 ∈ 𝑋 𝐶) |
60 | 59 | adantl 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 = ∅) → (2nd “
(𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)) = ∪
𝑥 ∈ 𝑋 𝐶) |
61 | | 2ndimaxp 31609 |
. . . . . . . . . 10
⊢ (𝑋 ≠ ∅ →
(2nd “ (𝑋
× ∪ 𝑥 ∈ 𝑋 𝐶)) = ∪
𝑥 ∈ 𝑋 𝐶) |
62 | 61 | adantl 483 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑋 ≠ ∅) → (2nd
“ (𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)) = ∪
𝑥 ∈ 𝑋 𝐶) |
63 | 60, 62 | pm2.61dane 3029 |
. . . . . . . 8
⊢ (𝜑 → (2nd “
(𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)) = ∪
𝑥 ∈ 𝑋 𝐶) |
64 | 63, 10 | eqtrd 2773 |
. . . . . . 7
⊢ (𝜑 → (2nd “
(𝑋 × ∪ 𝑥 ∈ 𝑋 𝐶)) = 𝐴) |
65 | 50, 64 | sseqtrid 3997 |
. . . . . 6
⊢ (𝜑 → (2nd “
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ 𝐴) |
66 | | resssxp 6223 |
. . . . . 6
⊢
((2nd “ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ 𝐴 ↔ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) × 𝐴)) |
67 | 65, 66 | sylib 217 |
. . . . 5
⊢ (𝜑 → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) × 𝐴)) |
68 | | dff2 7050 |
. . . . 5
⊢
((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶𝐴 ↔ ((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) Fn ∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ∧ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) ⊆ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) × 𝐴))) |
69 | 47, 67, 68 | sylanbrc 584 |
. . . 4
⊢ (𝜑 → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶𝐴) |
70 | 5, 69 | fcod 6695 |
. . 3
⊢ (𝜑 → (𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))):∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶𝐵) |
71 | 7, 4, 8, 9, 10 | 2ndresdju 31611 |
. . . 4
⊢ (𝜑 → (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)–1-1→𝐴) |
72 | 2 | fvexi 6857 |
. . . . 5
⊢ 0 ∈
V |
73 | 72 | a1i 11 |
. . . 4
⊢ (𝜑 → 0 ∈ V) |
74 | 5, 4 | fexd 7178 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ V) |
75 | 6, 71, 73, 74 | fsuppco 9343 |
. . 3
⊢ (𝜑 → (𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))) finSupp 0 ) |
76 | 1, 2, 3, 25, 30, 8, 39, 70, 75 | gsum2d 19754 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝐹 ∘ (2nd ↾
∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))) = (𝐺 Σg (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝑧 ∈ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧)))))) |
77 | | nfcsb1v 3881 |
. . . . . . . . 9
⊢
Ⅎ𝑥⦋𝑦 / 𝑥⦌𝐶 |
78 | | csbeq1a 3870 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑥⦌𝐶) |
79 | 8, 21, 77, 78 | iunsnima2 31584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) = ⦋𝑦 / 𝑥⦌𝐶) |
80 | | df-ov 7361 |
. . . . . . . . 9
⊢ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧) = ((𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))‘⟨𝑦, 𝑧⟩) |
81 | 69 | ad2antrr 725 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)):∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)⟶𝐴) |
82 | | simplr 768 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → 𝑦 ∈ 𝑋) |
83 | | vsnid 4624 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ∈ {𝑦} |
84 | 83 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → 𝑦 ∈ {𝑦}) |
85 | 79 | eleq2d 2820 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↔ 𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐶)) |
86 | 85 | biimpa 478 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → 𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐶) |
87 | 84, 86 | opelxpd 5672 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ⟨𝑦, 𝑧⟩ ∈ ({𝑦} × ⦋𝑦 / 𝑥⦌𝐶)) |
88 | | nfcv 2904 |
. . . . . . . . . . . . . . . 16
⊢
Ⅎ𝑥{𝑦} |
89 | 88, 77 | nfxp 5667 |
. . . . . . . . . . . . . . 15
⊢
Ⅎ𝑥({𝑦} × ⦋𝑦 / 𝑥⦌𝐶) |
90 | 89 | nfel2 2922 |
. . . . . . . . . . . . . 14
⊢
Ⅎ𝑥⟨𝑦, 𝑧⟩ ∈ ({𝑦} × ⦋𝑦 / 𝑥⦌𝐶) |
91 | | sneq 4597 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑦 → {𝑥} = {𝑦}) |
92 | 91, 78 | xpeq12d 5665 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑦 → ({𝑥} × 𝐶) = ({𝑦} × ⦋𝑦 / 𝑥⦌𝐶)) |
93 | 92 | eleq2d 2820 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑦 → (⟨𝑦, 𝑧⟩ ∈ ({𝑥} × 𝐶) ↔ ⟨𝑦, 𝑧⟩ ∈ ({𝑦} × ⦋𝑦 / 𝑥⦌𝐶))) |
94 | 90, 93 | rspce 3569 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ 𝑋 ∧ ⟨𝑦, 𝑧⟩ ∈ ({𝑦} × ⦋𝑦 / 𝑥⦌𝐶)) → ∃𝑥 ∈ 𝑋 ⟨𝑦, 𝑧⟩ ∈ ({𝑥} × 𝐶)) |
95 | 82, 87, 94 | syl2anc 585 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ∃𝑥 ∈ 𝑋 ⟨𝑦, 𝑧⟩ ∈ ({𝑥} × 𝐶)) |
96 | | eliun 4959 |
. . . . . . . . . . . 12
⊢
(⟨𝑦, 𝑧⟩ ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ↔ ∃𝑥 ∈ 𝑋 ⟨𝑦, 𝑧⟩ ∈ ({𝑥} × 𝐶)) |
97 | 95, 96 | sylibr 233 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ⟨𝑦, 𝑧⟩ ∈ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)) |
98 | 81, 97 | fvco3d 6942 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))‘⟨𝑦, 𝑧⟩) = (𝐹‘((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))‘⟨𝑦, 𝑧⟩))) |
99 | 97 | fvresd 6863 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))‘⟨𝑦, 𝑧⟩) = (2nd ‘⟨𝑦, 𝑧⟩)) |
100 | | vex 3448 |
. . . . . . . . . . . . 13
⊢ 𝑦 ∈ V |
101 | | vex 3448 |
. . . . . . . . . . . . 13
⊢ 𝑧 ∈ V |
102 | 100, 101 | op2nd 7931 |
. . . . . . . . . . . 12
⊢
(2nd ‘⟨𝑦, 𝑧⟩) = 𝑧 |
103 | 99, 102 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))‘⟨𝑦, 𝑧⟩) = 𝑧) |
104 | 103 | fveq2d 6847 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → (𝐹‘((2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶))‘⟨𝑦, 𝑧⟩)) = (𝐹‘𝑧)) |
105 | 98, 104 | eqtrd 2773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → ((𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))‘⟨𝑦, 𝑧⟩) = (𝐹‘𝑧)) |
106 | 80, 105 | eqtrid 2785 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝑋) ∧ 𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦})) → (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧) = (𝐹‘𝑧)) |
107 | 79, 106 | mpteq12dva 5195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧)) = (𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐶 ↦ (𝐹‘𝑧))) |
108 | 5 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → 𝐹:𝐴⟶𝐵) |
109 | | imassrn 6025 |
. . . . . . . . . 10
⊢ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ⊆ ran ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) |
110 | 10 | xpeq2d 5664 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑋 × ∪
𝑥 ∈ 𝑋 𝐶) = (𝑋 × 𝐴)) |
111 | 48, 110 | sseqtrid 3997 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴)) |
112 | | rnss 5895 |
. . . . . . . . . . . . 13
⊢ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ (𝑋 × 𝐴) → ran ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ ran (𝑋 × 𝐴)) |
113 | 111, 112 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ran ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ ran (𝑋 × 𝐴)) |
114 | 113 | adantr 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ran ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ ran (𝑋 × 𝐴)) |
115 | | rnxpss 6125 |
. . . . . . . . . . 11
⊢ ran
(𝑋 × 𝐴) ⊆ 𝐴 |
116 | 114, 115 | sstrdi 3957 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ran ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) ⊆ 𝐴) |
117 | 109, 116 | sstrid 3956 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ⊆ 𝐴) |
118 | 79, 117 | eqsstrrd 3984 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → ⦋𝑦 / 𝑥⦌𝐶 ⊆ 𝐴) |
119 | 108, 118 | feqresmpt 6912 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶) = (𝑧 ∈ ⦋𝑦 / 𝑥⦌𝐶 ↦ (𝐹‘𝑧))) |
120 | 107, 119 | eqtr4d 2776 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝑧 ∈ (∪
𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧)) = (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶)) |
121 | 120 | oveq2d 7374 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝑋) → (𝐺 Σg (𝑧 ∈ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧))) = (𝐺 Σg (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶))) |
122 | 121 | mpteq2dva 5206 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝑧 ∈ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧)))) = (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶)))) |
123 | | nfcv 2904 |
. . . . 5
⊢
Ⅎ𝑦(𝐺 Σg (𝐹 ↾ 𝐶)) |
124 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑥𝐺 |
125 | | nfcv 2904 |
. . . . . 6
⊢
Ⅎ𝑥
Σg |
126 | | nfcv 2904 |
. . . . . . 7
⊢
Ⅎ𝑥𝐹 |
127 | 126, 77 | nfres 5940 |
. . . . . 6
⊢
Ⅎ𝑥(𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶) |
128 | 124, 125,
127 | nfov 7388 |
. . . . 5
⊢
Ⅎ𝑥(𝐺 Σg (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶)) |
129 | 78 | reseq2d 5938 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐹 ↾ 𝐶) = (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶)) |
130 | 129 | oveq2d 7374 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐺 Σg (𝐹 ↾ 𝐶)) = (𝐺 Σg (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶))) |
131 | 123, 128,
130 | cbvmpt 5217 |
. . . 4
⊢ (𝑥 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ 𝐶))) = (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ ⦋𝑦 / 𝑥⦌𝐶))) |
132 | 122, 131 | eqtr4di 2791 |
. . 3
⊢ (𝜑 → (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝑧 ∈ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧)))) = (𝑥 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ 𝐶)))) |
133 | 132 | oveq2d 7374 |
. 2
⊢ (𝜑 → (𝐺 Σg (𝑦 ∈ 𝑋 ↦ (𝐺 Σg (𝑧 ∈ (∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶) “ {𝑦}) ↦ (𝑦(𝐹 ∘ (2nd ↾ ∪ 𝑥 ∈ 𝑋 ({𝑥} × 𝐶)))𝑧))))) = (𝐺 Σg (𝑥 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ 𝐶))))) |
134 | 12, 76, 133 | 3eqtrd 2777 |
1
⊢ (𝜑 → (𝐺 Σg 𝐹) = (𝐺 Σg (𝑥 ∈ 𝑋 ↦ (𝐺 Σg (𝐹 ↾ 𝐶))))) |