Step | Hyp | Ref
| Expression |
1 | | inss1 3795 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ 𝑊) ⊆ 𝐴 |
2 | | sspwb 4844 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∩ 𝑊) ⊆ 𝐴 ↔ 𝒫 (𝐴 ∩ 𝑊) ⊆ 𝒫 𝐴) |
3 | 1, 2 | mpbi 219 |
. . . . . . . . . . 11
⊢ 𝒫
(𝐴 ∩ 𝑊) ⊆ 𝒫 𝐴 |
4 | | ssrin 3800 |
. . . . . . . . . . 11
⊢
(𝒫 (𝐴 ∩
𝑊) ⊆ 𝒫 𝐴 → (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ⊆ (𝒫 𝐴 ∩ Fin)) |
5 | 3, 4 | ax-mp 5 |
. . . . . . . . . 10
⊢
(𝒫 (𝐴 ∩
𝑊) ∩ Fin) ⊆
(𝒫 𝐴 ∩
Fin) |
6 | | simpr 476 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) |
7 | 5, 6 | sseldi 3566 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) |
8 | | elfpw 8151 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin)) |
9 | 8 | simplbi 475 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ⊆ 𝐴) |
10 | 9 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑧 ⊆ 𝐴) |
11 | | ssrin 3800 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ⊆ 𝐴 → (𝑧 ∩ 𝑊) ⊆ (𝐴 ∩ 𝑊)) |
12 | 10, 11 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ∩ 𝑊) ⊆ (𝐴 ∩ 𝑊)) |
13 | 8 | simprbi 479 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ∈ Fin) |
14 | 13 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑧 ∈ Fin) |
15 | | inss1 3795 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∩ 𝑊) ⊆ 𝑧 |
16 | | ssfi 8065 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ Fin ∧ (𝑧 ∩ 𝑊) ⊆ 𝑧) → (𝑧 ∩ 𝑊) ∈ Fin) |
17 | 14, 15, 16 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ∩ 𝑊) ∈ Fin) |
18 | | elfpw 8151 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ↔ ((𝑧 ∩ 𝑊) ⊆ (𝐴 ∩ 𝑊) ∧ (𝑧 ∩ 𝑊) ∈ Fin)) |
19 | 12, 17, 18 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) |
20 | | sseq2 3590 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑧 ∩ 𝑊) → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ (𝑧 ∩ 𝑊))) |
21 | | ssin 3797 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊) ↔ 𝑎 ⊆ (𝑧 ∩ 𝑊)) |
22 | 20, 21 | syl6bbr 277 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑧 ∩ 𝑊) → (𝑎 ⊆ 𝑏 ↔ (𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊))) |
23 | | reseq2 5312 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑧 ∩ 𝑊) → ((𝐹 ↾ 𝑊) ↾ 𝑏) = ((𝐹 ↾ 𝑊) ↾ (𝑧 ∩ 𝑊))) |
24 | | inss2 3796 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∩ 𝑊) ⊆ 𝑊 |
25 | | resabs1 5347 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∩ 𝑊) ⊆ 𝑊 → ((𝐹 ↾ 𝑊) ↾ (𝑧 ∩ 𝑊)) = (𝐹 ↾ (𝑧 ∩ 𝑊))) |
26 | 24, 25 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ↾ 𝑊) ↾ (𝑧 ∩ 𝑊)) = (𝐹 ↾ (𝑧 ∩ 𝑊)) |
27 | 23, 26 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑧 ∩ 𝑊) → ((𝐹 ↾ 𝑊) ↾ 𝑏) = (𝐹 ↾ (𝑧 ∩ 𝑊))) |
28 | 27 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑧 ∩ 𝑊) → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) = (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊)))) |
29 | 28 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑧 ∩ 𝑊) → ((𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢)) |
30 | 22, 29 | imbi12d 333 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑧 ∩ 𝑊) → ((𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) ↔ ((𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊) → (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢))) |
31 | 30 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) → (∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → ((𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊) → (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢))) |
32 | 19, 31 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → ((𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊) → (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢))) |
33 | | elfpw 8151 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ↔ (𝑎 ⊆ (𝐴 ∩ 𝑊) ∧ 𝑎 ∈ Fin)) |
34 | 33 | simplbi 475 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) → 𝑎 ⊆ (𝐴 ∩ 𝑊)) |
35 | 34 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ⊆ (𝐴 ∩ 𝑊)) |
36 | | inss2 3796 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∩ 𝑊) ⊆ 𝑊 |
37 | 35, 36 | syl6ss 3580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ⊆ 𝑊) |
38 | 37 | biantrud 527 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑎 ⊆ 𝑧 ↔ (𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊))) |
39 | | resres 5329 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ↾ 𝑧) ↾ 𝑊) = (𝐹 ↾ (𝑧 ∩ 𝑊)) |
40 | 39 | oveq2i 6560 |
. . . . . . . . . . . . . 14
⊢ (𝐺 Σg
((𝐹 ↾ 𝑧) ↾ 𝑊)) = (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) |
41 | | tsmsres.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝐺) |
42 | | tsmsres.z |
. . . . . . . . . . . . . . 15
⊢ 0 =
(0g‘𝐺) |
43 | | tsmsres.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺 ∈ CMnd) |
44 | 43 | ad2antrr 758 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd) |
45 | | tsmsres.f |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
46 | 45 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐴⟶𝐵) |
47 | 46, 10 | fssresd 5984 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑧):𝑧⟶𝐵) |
48 | | tsmsres.a |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
49 | | fex 6394 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
50 | 45, 48, 49 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ V) |
51 | 50 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹 ∈ V) |
52 | | fvex 6113 |
. . . . . . . . . . . . . . . . . 18
⊢
(0g‘𝐺) ∈ V |
53 | 42, 52 | eqeltri 2684 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
V |
54 | | ressuppss 7201 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ ((𝐹 ↾ 𝑧) supp 0 ) ⊆ (𝐹 supp 0 )) |
55 | 51, 53, 54 | sylancl 693 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ 𝑧) supp 0 ) ⊆ (𝐹 supp 0 )) |
56 | | tsmsres.s |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊) |
57 | 56 | ad2antrr 758 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 supp 0 ) ⊆ 𝑊) |
58 | 55, 57 | sstrd 3578 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ 𝑧) supp 0 ) ⊆ 𝑊) |
59 | 53 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈ V) |
60 | 47, 14, 59 | fdmfifsupp 8168 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑧) finSupp 0 ) |
61 | 41, 42, 44, 14, 47, 58, 60 | gsumres 18137 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg ((𝐹 ↾ 𝑧) ↾ 𝑊)) = (𝐺 Σg (𝐹 ↾ 𝑧))) |
62 | 40, 61 | syl5reqr 2659 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑧)) = (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊)))) |
63 | 62 | eleq1d 2672 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢)) |
64 | 38, 63 | imbi12d 333 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝑎 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ ((𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊) → (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢))) |
65 | 32, 64 | sylibrd 248 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → (𝑎 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
66 | 65 | ralrimdva 2952 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → ∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
67 | | sseq1 3589 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑎 → (𝑦 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑧)) |
68 | 67 | imbi1d 330 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑎 → ((𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝑎 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
69 | 68 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑎 → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ ∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
70 | 69 | rspcev 3282 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
71 | 7, 66, 70 | syl6an 566 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
72 | 71 | rexlimdva 3013 |
. . . . . . 7
⊢ (𝜑 → (∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
73 | | elfpw 8151 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin)) |
74 | 73 | simplbi 475 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴) |
75 | 74 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴) |
76 | | ssrin 3800 |
. . . . . . . . . . 11
⊢ (𝑦 ⊆ 𝐴 → (𝑦 ∩ 𝑊) ⊆ (𝐴 ∩ 𝑊)) |
77 | 75, 76 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑦 ∩ 𝑊) ⊆ (𝐴 ∩ 𝑊)) |
78 | 73 | simprbi 479 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin) |
79 | 78 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin) |
80 | | inss1 3795 |
. . . . . . . . . . 11
⊢ (𝑦 ∩ 𝑊) ⊆ 𝑦 |
81 | | ssfi 8065 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ Fin ∧ (𝑦 ∩ 𝑊) ⊆ 𝑦) → (𝑦 ∩ 𝑊) ∈ Fin) |
82 | 79, 80, 81 | sylancl 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑦 ∩ 𝑊) ∈ Fin) |
83 | | elfpw 8151 |
. . . . . . . . . 10
⊢ ((𝑦 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ↔ ((𝑦 ∩ 𝑊) ⊆ (𝐴 ∩ 𝑊) ∧ (𝑦 ∩ 𝑊) ∈ Fin)) |
84 | 77, 82, 83 | sylanbrc 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑦 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) |
85 | 74 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑦 ⊆ 𝐴) |
86 | | elfpw 8151 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ↔ (𝑏 ⊆ (𝐴 ∩ 𝑊) ∧ 𝑏 ∈ Fin)) |
87 | 86 | simplbi 475 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) → 𝑏 ⊆ (𝐴 ∩ 𝑊)) |
88 | 87 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑏 ⊆ (𝐴 ∩ 𝑊)) |
89 | 88, 1 | syl6ss 3580 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑏 ⊆ 𝐴) |
90 | 85, 89 | unssd 3751 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (𝑦 ∪ 𝑏) ⊆ 𝐴) |
91 | 86 | simprbi 479 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) → 𝑏 ∈ Fin) |
92 | | unfi 8112 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ Fin ∧ 𝑏 ∈ Fin) → (𝑦 ∪ 𝑏) ∈ Fin) |
93 | 79, 91, 92 | syl2an 493 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (𝑦 ∪ 𝑏) ∈ Fin) |
94 | | elfpw 8151 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∪ 𝑏) ∈ (𝒫 𝐴 ∩ Fin) ↔ ((𝑦 ∪ 𝑏) ⊆ 𝐴 ∧ (𝑦 ∪ 𝑏) ∈ Fin)) |
95 | 90, 93, 94 | sylanbrc 695 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (𝑦 ∪ 𝑏) ∈ (𝒫 𝐴 ∩ Fin)) |
96 | | ssun1 3738 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ⊆ (𝑦 ∪ 𝑏) |
97 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑦 ∪ 𝑏) → 𝑧 = (𝑦 ∪ 𝑏)) |
98 | 96, 97 | syl5sseqr 3617 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 ∪ 𝑏) → 𝑦 ⊆ 𝑧) |
99 | | pm5.5 350 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ⊆ 𝑧 → ((𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
100 | 98, 99 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦 ∪ 𝑏) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
101 | | reseq2 5312 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑦 ∪ 𝑏) → (𝐹 ↾ 𝑧) = (𝐹 ↾ (𝑦 ∪ 𝑏))) |
102 | 101 | oveq2d 6565 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 ∪ 𝑏) → (𝐺 Σg (𝐹 ↾ 𝑧)) = (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏)))) |
103 | 102 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦 ∪ 𝑏) → ((𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢)) |
104 | 100, 103 | bitrd 267 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑦 ∪ 𝑏) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢)) |
105 | 104 | rspcv 3278 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∪ 𝑏) ∈ (𝒫 𝐴 ∩ Fin) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢)) |
106 | 95, 105 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢)) |
107 | 43 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → 𝐺 ∈ CMnd) |
108 | 93 | adantrr 749 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝑦 ∪ 𝑏) ∈ Fin) |
109 | 45 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → 𝐹:𝐴⟶𝐵) |
110 | 90 | adantrr 749 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝑦 ∪ 𝑏) ⊆ 𝐴) |
111 | 109, 110 | fssresd 5984 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐹 ↾ (𝑦 ∪ 𝑏)):(𝑦 ∪ 𝑏)⟶𝐵) |
112 | 50, 53 | jctir 559 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐹 ∈ V ∧ 0 ∈
V)) |
113 | 112 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐹 ∈ V ∧ 0 ∈
V)) |
114 | | ressuppss 7201 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ ((𝐹 ↾ (𝑦 ∪ 𝑏)) supp 0 ) ⊆ (𝐹 supp 0 )) |
115 | 113, 114 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐹 ↾ (𝑦 ∪ 𝑏)) supp 0 ) ⊆ (𝐹 supp 0 )) |
116 | 56 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐹 supp 0 ) ⊆ 𝑊) |
117 | 115, 116 | sstrd 3578 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐹 ↾ (𝑦 ∪ 𝑏)) supp 0 ) ⊆ 𝑊) |
118 | 53 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → 0 ∈ V) |
119 | 111, 108,
118 | fdmfifsupp 8168 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐹 ↾ (𝑦 ∪ 𝑏)) finSupp 0 ) |
120 | 41, 42, 107, 108, 111, 117, 119 | gsumres 18137 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐺 Σg ((𝐹 ↾ (𝑦 ∪ 𝑏)) ↾ 𝑊)) = (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏)))) |
121 | | resres 5329 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ↾ (𝑦 ∪ 𝑏)) ↾ 𝑊) = (𝐹 ↾ ((𝑦 ∪ 𝑏) ∩ 𝑊)) |
122 | | indir 3834 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∪ 𝑏) ∩ 𝑊) = ((𝑦 ∩ 𝑊) ∪ (𝑏 ∩ 𝑊)) |
123 | 88, 36 | syl6ss 3580 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑏 ⊆ 𝑊) |
124 | 123 | adantrr 749 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → 𝑏 ⊆ 𝑊) |
125 | | df-ss 3554 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ⊆ 𝑊 ↔ (𝑏 ∩ 𝑊) = 𝑏) |
126 | 124, 125 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝑏 ∩ 𝑊) = 𝑏) |
127 | 126 | uneq2d 3729 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝑦 ∩ 𝑊) ∪ (𝑏 ∩ 𝑊)) = ((𝑦 ∩ 𝑊) ∪ 𝑏)) |
128 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝑦 ∩ 𝑊) ⊆ 𝑏) |
129 | | ssequn1 3745 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∩ 𝑊) ⊆ 𝑏 ↔ ((𝑦 ∩ 𝑊) ∪ 𝑏) = 𝑏) |
130 | 128, 129 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝑦 ∩ 𝑊) ∪ 𝑏) = 𝑏) |
131 | 127, 130 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝑦 ∩ 𝑊) ∪ (𝑏 ∩ 𝑊)) = 𝑏) |
132 | 122, 131 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝑦 ∪ 𝑏) ∩ 𝑊) = 𝑏) |
133 | 132 | reseq2d 5317 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐹 ↾ ((𝑦 ∪ 𝑏) ∩ 𝑊)) = (𝐹 ↾ 𝑏)) |
134 | 121, 133 | syl5eq 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐹 ↾ (𝑦 ∪ 𝑏)) ↾ 𝑊) = (𝐹 ↾ 𝑏)) |
135 | 124 | resabs1d 5348 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐹 ↾ 𝑊) ↾ 𝑏) = (𝐹 ↾ 𝑏)) |
136 | 134, 135 | eqtr4d 2647 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐹 ↾ (𝑦 ∪ 𝑏)) ↾ 𝑊) = ((𝐹 ↾ 𝑊) ↾ 𝑏)) |
137 | 136 | oveq2d 6565 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐺 Σg ((𝐹 ↾ (𝑦 ∪ 𝑏)) ↾ 𝑊)) = (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏))) |
138 | 120, 137 | eqtr3d 2646 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) = (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏))) |
139 | 138 | eleq1d 2672 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢 ↔ (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) |
140 | 139 | biimpd 218 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) |
141 | 140 | expr 641 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → ((𝑦 ∩ 𝑊) ⊆ 𝑏 → ((𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
142 | 141 | com23 84 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢 → ((𝑦 ∩ 𝑊) ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
143 | 106, 142 | syld 46 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → ((𝑦 ∩ 𝑊) ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
144 | 143 | ralrimdva 2952 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → ∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)((𝑦 ∩ 𝑊) ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
145 | | sseq1 3589 |
. . . . . . . . . . . 12
⊢ (𝑎 = (𝑦 ∩ 𝑊) → (𝑎 ⊆ 𝑏 ↔ (𝑦 ∩ 𝑊) ⊆ 𝑏)) |
146 | 145 | imbi1d 330 |
. . . . . . . . . . 11
⊢ (𝑎 = (𝑦 ∩ 𝑊) → ((𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) ↔ ((𝑦 ∩ 𝑊) ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
147 | 146 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑦 ∩ 𝑊) → (∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) ↔ ∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)((𝑦 ∩ 𝑊) ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
148 | 147 | rspcev 3282 |
. . . . . . . . 9
⊢ (((𝑦 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ ∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)((𝑦 ∩ 𝑊) ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) |
149 | 84, 144, 148 | syl6an 566 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
150 | 149 | rexlimdva 3013 |
. . . . . . 7
⊢ (𝜑 → (∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
151 | 72, 150 | impbid 201 |
. . . . . 6
⊢ (𝜑 → (∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) ↔ ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
152 | 151 | imbi2d 329 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) ↔ (𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)))) |
153 | 152 | ralbidv 2969 |
. . . 4
⊢ (𝜑 → (∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) ↔ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)))) |
154 | 153 | anbi2d 736 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))))) |
155 | | eqid 2610 |
. . . 4
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) |
156 | | eqid 2610 |
. . . 4
⊢
(𝒫 (𝐴 ∩
𝑊) ∩ Fin) = (𝒫
(𝐴 ∩ 𝑊) ∩ Fin) |
157 | | tsmsres.2 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TopSp) |
158 | | inex1g 4729 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝑊) ∈ V) |
159 | 48, 158 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐴 ∩ 𝑊) ∈ V) |
160 | | fssres 5983 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐴 ∩ 𝑊) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵) |
161 | 45, 1, 160 | sylancl 693 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵) |
162 | | resres 5329 |
. . . . . . 7
⊢ ((𝐹 ↾ 𝐴) ↾ 𝑊) = (𝐹 ↾ (𝐴 ∩ 𝑊)) |
163 | | ffn 5958 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
164 | | fnresdm 5914 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
165 | 45, 163, 164 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ↾ 𝐴) = 𝐹) |
166 | 165 | reseq1d 5316 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑊) = (𝐹 ↾ 𝑊)) |
167 | 162, 166 | syl5eqr 2658 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑊)) = (𝐹 ↾ 𝑊)) |
168 | 167 | feq1d 5943 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵 ↔ (𝐹 ↾ 𝑊):(𝐴 ∩ 𝑊)⟶𝐵)) |
169 | 161, 168 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ 𝑊):(𝐴 ∩ 𝑊)⟶𝐵) |
170 | 41, 155, 156, 43, 157, 159, 169 | eltsms 21746 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums (𝐹 ↾ 𝑊)) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))))) |
171 | | eqid 2610 |
. . . 4
⊢
(𝒫 𝐴 ∩
Fin) = (𝒫 𝐴 ∩
Fin) |
172 | 41, 155, 171, 43, 157, 48, 45 | eltsms 21746 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))))) |
173 | 154, 170,
172 | 3bitr4d 299 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums (𝐹 ↾ 𝑊)) ↔ 𝑥 ∈ (𝐺 tsums 𝐹))) |
174 | 173 | eqrdv 2608 |
1
⊢ (𝜑 → (𝐺 tsums (𝐹 ↾ 𝑊)) = (𝐺 tsums 𝐹)) |