Step | Hyp | Ref
| Expression |
1 | | inss1 4208 |
. . . . . . . . . . . 12
⊢ (𝐴 ∩ 𝑊) ⊆ 𝐴 |
2 | 1 | sspwi 4556 |
. . . . . . . . . . 11
⊢ 𝒫
(𝐴 ∩ 𝑊) ⊆ 𝒫 𝐴 |
3 | | ssrin 4213 |
. . . . . . . . . . 11
⊢
(𝒫 (𝐴 ∩
𝑊) ⊆ 𝒫 𝐴 → (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ⊆ (𝒫 𝐴 ∩ Fin)) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . . . 10
⊢
(𝒫 (𝐴 ∩
𝑊) ∩ Fin) ⊆
(𝒫 𝐴 ∩
Fin) |
5 | | simpr 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) |
6 | 4, 5 | sseldi 3968 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑎 ∈ (𝒫 𝐴 ∩ Fin)) |
7 | | elfpw 8829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin)) |
8 | 7 | simplbi 500 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ⊆ 𝐴) |
9 | 8 | adantl 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑧 ⊆ 𝐴) |
10 | 9 | ssrind 4215 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ∩ 𝑊) ⊆ (𝐴 ∩ 𝑊)) |
11 | | elinel2 4176 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) → 𝑧 ∈ Fin) |
12 | 11 | adantl 484 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑧 ∈ Fin) |
13 | | inss1 4208 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∩ 𝑊) ⊆ 𝑧 |
14 | | ssfi 8741 |
. . . . . . . . . . . . . 14
⊢ ((𝑧 ∈ Fin ∧ (𝑧 ∩ 𝑊) ⊆ 𝑧) → (𝑧 ∩ 𝑊) ∈ Fin) |
15 | 12, 13, 14 | sylancl 588 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ∩ 𝑊) ∈ Fin) |
16 | | elfpw 8829 |
. . . . . . . . . . . . 13
⊢ ((𝑧 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ↔ ((𝑧 ∩ 𝑊) ⊆ (𝐴 ∩ 𝑊) ∧ (𝑧 ∩ 𝑊) ∈ Fin)) |
17 | 10, 15, 16 | sylanbrc 585 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑧 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) |
18 | | sseq2 3996 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑧 ∩ 𝑊) → (𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ (𝑧 ∩ 𝑊))) |
19 | | ssin 4210 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊) ↔ 𝑎 ⊆ (𝑧 ∩ 𝑊)) |
20 | 18, 19 | syl6bbr 291 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑧 ∩ 𝑊) → (𝑎 ⊆ 𝑏 ↔ (𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊))) |
21 | | reseq2 5851 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = (𝑧 ∩ 𝑊) → ((𝐹 ↾ 𝑊) ↾ 𝑏) = ((𝐹 ↾ 𝑊) ↾ (𝑧 ∩ 𝑊))) |
22 | | inss2 4209 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 ∩ 𝑊) ⊆ 𝑊 |
23 | | resabs1 5886 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑧 ∩ 𝑊) ⊆ 𝑊 → ((𝐹 ↾ 𝑊) ↾ (𝑧 ∩ 𝑊)) = (𝐹 ↾ (𝑧 ∩ 𝑊))) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ↾ 𝑊) ↾ (𝑧 ∩ 𝑊)) = (𝐹 ↾ (𝑧 ∩ 𝑊)) |
25 | 21, 24 | syl6eq 2875 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = (𝑧 ∩ 𝑊) → ((𝐹 ↾ 𝑊) ↾ 𝑏) = (𝐹 ↾ (𝑧 ∩ 𝑊))) |
26 | 25 | oveq2d 7175 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑧 ∩ 𝑊) → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) = (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊)))) |
27 | 26 | eleq1d 2900 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = (𝑧 ∩ 𝑊) → ((𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢)) |
28 | 20, 27 | imbi12d 347 |
. . . . . . . . . . . . 13
⊢ (𝑏 = (𝑧 ∩ 𝑊) → ((𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) ↔ ((𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊) → (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢))) |
29 | 28 | rspcv 3621 |
. . . . . . . . . . . 12
⊢ ((𝑧 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) → (∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → ((𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊) → (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢))) |
30 | 17, 29 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → ((𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊) → (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢))) |
31 | | elfpw 8829 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ↔ (𝑎 ⊆ (𝐴 ∩ 𝑊) ∧ 𝑎 ∈ Fin)) |
32 | 31 | simplbi 500 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) → 𝑎 ⊆ (𝐴 ∩ 𝑊)) |
33 | 32 | ad2antlr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ⊆ (𝐴 ∩ 𝑊)) |
34 | | inss2 4209 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∩ 𝑊) ⊆ 𝑊 |
35 | 33, 34 | sstrdi 3982 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑎 ⊆ 𝑊) |
36 | 35 | biantrud 534 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑎 ⊆ 𝑧 ↔ (𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊))) |
37 | | resres 5869 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 ↾ 𝑧) ↾ 𝑊) = (𝐹 ↾ (𝑧 ∩ 𝑊)) |
38 | 37 | oveq2i 7170 |
. . . . . . . . . . . . . 14
⊢ (𝐺 Σg
((𝐹 ↾ 𝑧) ↾ 𝑊)) = (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) |
39 | | tsmsres.b |
. . . . . . . . . . . . . . 15
⊢ 𝐵 = (Base‘𝐺) |
40 | | tsmsres.z |
. . . . . . . . . . . . . . 15
⊢ 0 =
(0g‘𝐺) |
41 | | tsmsres.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐺 ∈ CMnd) |
42 | 41 | ad2antrr 724 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd) |
43 | | tsmsres.f |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
44 | 43 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐴⟶𝐵) |
45 | 44, 9 | fssresd 6548 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑧):𝑧⟶𝐵) |
46 | | tsmsres.a |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
47 | | fex 6992 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐴 ∈ 𝑉) → 𝐹 ∈ V) |
48 | 43, 46, 47 | syl2anc 586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝐹 ∈ V) |
49 | 48 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹 ∈ V) |
50 | 40 | fvexi 6687 |
. . . . . . . . . . . . . . . . 17
⊢ 0 ∈
V |
51 | | ressuppss 7852 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ ((𝐹 ↾ 𝑧) supp 0 ) ⊆ (𝐹 supp 0 )) |
52 | 49, 50, 51 | sylancl 588 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ 𝑧) supp 0 ) ⊆ (𝐹 supp 0 )) |
53 | | tsmsres.s |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝑊) |
54 | 53 | ad2antrr 724 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 supp 0 ) ⊆ 𝑊) |
55 | 52, 54 | sstrd 3980 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 ↾ 𝑧) supp 0 ) ⊆ 𝑊) |
56 | 50 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → 0 ∈ V) |
57 | 45, 12, 56 | fdmfifsupp 8846 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 ↾ 𝑧) finSupp 0 ) |
58 | 39, 40, 42, 12, 45, 55, 57 | gsumres 19036 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg ((𝐹 ↾ 𝑧) ↾ 𝑊)) = (𝐺 Σg (𝐹 ↾ 𝑧))) |
59 | 38, 58 | syl5reqr 2874 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ 𝑧)) = (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊)))) |
60 | 59 | eleq1d 2900 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢)) |
61 | 36, 60 | imbi12d 347 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝑎 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ ((𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊) → (𝐺 Σg (𝐹 ↾ (𝑧 ∩ 𝑊))) ∈ 𝑢))) |
62 | 30, 61 | sylibrd 261 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → (∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → (𝑎 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
63 | 62 | ralrimdva 3192 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → ∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
64 | | sseq1 3995 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑎 → (𝑦 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑧)) |
65 | 64 | rspceaimv 3631 |
. . . . . . . . 9
⊢ ((𝑎 ∈ (𝒫 𝐴 ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑎 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
66 | 6, 63, 65 | syl6an 682 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
67 | 66 | rexlimdva 3287 |
. . . . . . 7
⊢ (𝜑 → (∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
68 | | elfpw 8829 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin)) |
69 | 68 | simplbi 500 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴) |
70 | 69 | adantl 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴) |
71 | 70 | ssrind 4215 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑦 ∩ 𝑊) ⊆ (𝐴 ∩ 𝑊)) |
72 | | elinel2 4176 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin) |
73 | 72 | adantl 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin) |
74 | | inss1 4208 |
. . . . . . . . . . 11
⊢ (𝑦 ∩ 𝑊) ⊆ 𝑦 |
75 | | ssfi 8741 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ Fin ∧ (𝑦 ∩ 𝑊) ⊆ 𝑦) → (𝑦 ∩ 𝑊) ∈ Fin) |
76 | 73, 74, 75 | sylancl 588 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑦 ∩ 𝑊) ∈ Fin) |
77 | | elfpw 8829 |
. . . . . . . . . 10
⊢ ((𝑦 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ↔ ((𝑦 ∩ 𝑊) ⊆ (𝐴 ∩ 𝑊) ∧ (𝑦 ∩ 𝑊) ∈ Fin)) |
78 | 71, 76, 77 | sylanbrc 585 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑦 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) |
79 | 69 | ad2antlr 725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑦 ⊆ 𝐴) |
80 | | elfpw 8829 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ↔ (𝑏 ⊆ (𝐴 ∩ 𝑊) ∧ 𝑏 ∈ Fin)) |
81 | 80 | simplbi 500 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) → 𝑏 ⊆ (𝐴 ∩ 𝑊)) |
82 | 81 | adantl 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑏 ⊆ (𝐴 ∩ 𝑊)) |
83 | 82, 1 | sstrdi 3982 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑏 ⊆ 𝐴) |
84 | 79, 83 | unssd 4165 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (𝑦 ∪ 𝑏) ⊆ 𝐴) |
85 | | elinel2 4176 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) → 𝑏 ∈ Fin) |
86 | | unfi 8788 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ Fin ∧ 𝑏 ∈ Fin) → (𝑦 ∪ 𝑏) ∈ Fin) |
87 | 73, 85, 86 | syl2an 597 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (𝑦 ∪ 𝑏) ∈ Fin) |
88 | | elfpw 8829 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∪ 𝑏) ∈ (𝒫 𝐴 ∩ Fin) ↔ ((𝑦 ∪ 𝑏) ⊆ 𝐴 ∧ (𝑦 ∪ 𝑏) ∈ Fin)) |
89 | 84, 87, 88 | sylanbrc 585 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (𝑦 ∪ 𝑏) ∈ (𝒫 𝐴 ∩ Fin)) |
90 | | ssun1 4151 |
. . . . . . . . . . . . . . . 16
⊢ 𝑦 ⊆ (𝑦 ∪ 𝑏) |
91 | | id 22 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑦 ∪ 𝑏) → 𝑧 = (𝑦 ∪ 𝑏)) |
92 | 90, 91 | sseqtrrid 4023 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 ∪ 𝑏) → 𝑦 ⊆ 𝑧) |
93 | | pm5.5 364 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ⊆ 𝑧 → ((𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦 ∪ 𝑏) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
95 | | reseq2 5851 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑦 ∪ 𝑏) → (𝐹 ↾ 𝑧) = (𝐹 ↾ (𝑦 ∪ 𝑏))) |
96 | 95 | oveq2d 7175 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 ∪ 𝑏) → (𝐺 Σg (𝐹 ↾ 𝑧)) = (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏)))) |
97 | 96 | eleq1d 2900 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦 ∪ 𝑏) → ((𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢)) |
98 | 94, 97 | bitrd 281 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑦 ∪ 𝑏) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢)) |
99 | 98 | rspcv 3621 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∪ 𝑏) ∈ (𝒫 𝐴 ∩ Fin) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢)) |
100 | 89, 99 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢)) |
101 | 41 | ad2antrr 724 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → 𝐺 ∈ CMnd) |
102 | 87 | adantrr 715 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝑦 ∪ 𝑏) ∈ Fin) |
103 | 43 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → 𝐹:𝐴⟶𝐵) |
104 | 84 | adantrr 715 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝑦 ∪ 𝑏) ⊆ 𝐴) |
105 | 103, 104 | fssresd 6548 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐹 ↾ (𝑦 ∪ 𝑏)):(𝑦 ∪ 𝑏)⟶𝐵) |
106 | 48, 50 | jctir 523 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (𝐹 ∈ V ∧ 0 ∈
V)) |
107 | 106 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐹 ∈ V ∧ 0 ∈
V)) |
108 | | ressuppss 7852 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ∈ V ∧ 0 ∈ V)
→ ((𝐹 ↾ (𝑦 ∪ 𝑏)) supp 0 ) ⊆ (𝐹 supp 0 )) |
109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐹 ↾ (𝑦 ∪ 𝑏)) supp 0 ) ⊆ (𝐹 supp 0 )) |
110 | 53 | ad2antrr 724 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐹 supp 0 ) ⊆ 𝑊) |
111 | 109, 110 | sstrd 3980 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐹 ↾ (𝑦 ∪ 𝑏)) supp 0 ) ⊆ 𝑊) |
112 | 50 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → 0 ∈ V) |
113 | 105, 102,
112 | fdmfifsupp 8846 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐹 ↾ (𝑦 ∪ 𝑏)) finSupp 0 ) |
114 | 39, 40, 101, 102, 105, 111, 113 | gsumres 19036 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐺 Σg ((𝐹 ↾ (𝑦 ∪ 𝑏)) ↾ 𝑊)) = (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏)))) |
115 | | resres 5869 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹 ↾ (𝑦 ∪ 𝑏)) ↾ 𝑊) = (𝐹 ↾ ((𝑦 ∪ 𝑏) ∩ 𝑊)) |
116 | | indir 4255 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∪ 𝑏) ∩ 𝑊) = ((𝑦 ∩ 𝑊) ∪ (𝑏 ∩ 𝑊)) |
117 | 82, 34 | sstrdi 3982 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → 𝑏 ⊆ 𝑊) |
118 | 117 | adantrr 715 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → 𝑏 ⊆ 𝑊) |
119 | | df-ss 3955 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑏 ⊆ 𝑊 ↔ (𝑏 ∩ 𝑊) = 𝑏) |
120 | 118, 119 | sylib 220 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝑏 ∩ 𝑊) = 𝑏) |
121 | 120 | uneq2d 4142 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝑦 ∩ 𝑊) ∪ (𝑏 ∩ 𝑊)) = ((𝑦 ∩ 𝑊) ∪ 𝑏)) |
122 | | simprr 771 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝑦 ∩ 𝑊) ⊆ 𝑏) |
123 | | ssequn1 4159 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∩ 𝑊) ⊆ 𝑏 ↔ ((𝑦 ∩ 𝑊) ∪ 𝑏) = 𝑏) |
124 | 122, 123 | sylib 220 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝑦 ∩ 𝑊) ∪ 𝑏) = 𝑏) |
125 | 121, 124 | eqtrd 2859 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝑦 ∩ 𝑊) ∪ (𝑏 ∩ 𝑊)) = 𝑏) |
126 | 116, 125 | syl5eq 2871 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝑦 ∪ 𝑏) ∩ 𝑊) = 𝑏) |
127 | 126 | reseq2d 5856 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐹 ↾ ((𝑦 ∪ 𝑏) ∩ 𝑊)) = (𝐹 ↾ 𝑏)) |
128 | 115, 127 | syl5eq 2871 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐹 ↾ (𝑦 ∪ 𝑏)) ↾ 𝑊) = (𝐹 ↾ 𝑏)) |
129 | 118 | resabs1d 5887 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐹 ↾ 𝑊) ↾ 𝑏) = (𝐹 ↾ 𝑏)) |
130 | 128, 129 | eqtr4d 2862 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐹 ↾ (𝑦 ∪ 𝑏)) ↾ 𝑊) = ((𝐹 ↾ 𝑊) ↾ 𝑏)) |
131 | 130 | oveq2d 7175 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐺 Σg ((𝐹 ↾ (𝑦 ∪ 𝑏)) ↾ 𝑊)) = (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏))) |
132 | 114, 131 | eqtr3d 2861 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → (𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) = (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏))) |
133 | 132 | eleq1d 2900 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢 ↔ (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) |
134 | 133 | biimpd 231 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ (𝑦 ∩ 𝑊) ⊆ 𝑏)) → ((𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) |
135 | 134 | expr 459 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → ((𝑦 ∩ 𝑊) ⊆ 𝑏 → ((𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
136 | 135 | com23 86 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ (𝑦 ∪ 𝑏))) ∈ 𝑢 → ((𝑦 ∩ 𝑊) ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
137 | 100, 136 | syld 47 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → ((𝑦 ∩ 𝑊) ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
138 | 137 | ralrimdva 3192 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → ∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)((𝑦 ∩ 𝑊) ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
139 | | sseq1 3995 |
. . . . . . . . . 10
⊢ (𝑎 = (𝑦 ∩ 𝑊) → (𝑎 ⊆ 𝑏 ↔ (𝑦 ∩ 𝑊) ⊆ 𝑏)) |
140 | 139 | rspceaimv 3631 |
. . . . . . . . 9
⊢ (((𝑦 ∩ 𝑊) ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin) ∧ ∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)((𝑦 ∩ 𝑊) ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) |
141 | 78, 138, 140 | syl6an 682 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
142 | 141 | rexlimdva 3287 |
. . . . . . 7
⊢ (𝜑 → (∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) |
143 | 67, 142 | impbid 214 |
. . . . . 6
⊢ (𝜑 → (∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢) ↔ ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
144 | 143 | imbi2d 343 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) ↔ (𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)))) |
145 | 144 | ralbidv 3200 |
. . . 4
⊢ (𝜑 → (∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢)) ↔ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)))) |
146 | 145 | anbi2d 630 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))))) |
147 | | eqid 2824 |
. . . 4
⊢
(TopOpen‘𝐺) =
(TopOpen‘𝐺) |
148 | | eqid 2824 |
. . . 4
⊢
(𝒫 (𝐴 ∩
𝑊) ∩ Fin) = (𝒫
(𝐴 ∩ 𝑊) ∩ Fin) |
149 | | tsmsres.2 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ TopSp) |
150 | | inex1g 5226 |
. . . . 5
⊢ (𝐴 ∈ 𝑉 → (𝐴 ∩ 𝑊) ∈ V) |
151 | 46, 150 | syl 17 |
. . . 4
⊢ (𝜑 → (𝐴 ∩ 𝑊) ∈ V) |
152 | | fssres 6547 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ (𝐴 ∩ 𝑊) ⊆ 𝐴) → (𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵) |
153 | 43, 1, 152 | sylancl 588 |
. . . . 5
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵) |
154 | | resres 5869 |
. . . . . . 7
⊢ ((𝐹 ↾ 𝐴) ↾ 𝑊) = (𝐹 ↾ (𝐴 ∩ 𝑊)) |
155 | | ffn 6517 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
156 | | fnresdm 6469 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐴 → (𝐹 ↾ 𝐴) = 𝐹) |
157 | 43, 155, 156 | 3syl 18 |
. . . . . . . 8
⊢ (𝜑 → (𝐹 ↾ 𝐴) = 𝐹) |
158 | 157 | reseq1d 5855 |
. . . . . . 7
⊢ (𝜑 → ((𝐹 ↾ 𝐴) ↾ 𝑊) = (𝐹 ↾ 𝑊)) |
159 | 154, 158 | syl5eqr 2873 |
. . . . . 6
⊢ (𝜑 → (𝐹 ↾ (𝐴 ∩ 𝑊)) = (𝐹 ↾ 𝑊)) |
160 | 159 | feq1d 6502 |
. . . . 5
⊢ (𝜑 → ((𝐹 ↾ (𝐴 ∩ 𝑊)):(𝐴 ∩ 𝑊)⟶𝐵 ↔ (𝐹 ↾ 𝑊):(𝐴 ∩ 𝑊)⟶𝐵)) |
161 | 153, 160 | mpbid 234 |
. . . 4
⊢ (𝜑 → (𝐹 ↾ 𝑊):(𝐴 ∩ 𝑊)⟶𝐵) |
162 | 39, 147, 148, 41, 149, 151, 161 | eltsms 22744 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums (𝐹 ↾ 𝑊)) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑎 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)∀𝑏 ∈ (𝒫 (𝐴 ∩ 𝑊) ∩ Fin)(𝑎 ⊆ 𝑏 → (𝐺 Σg ((𝐹 ↾ 𝑊) ↾ 𝑏)) ∈ 𝑢))))) |
163 | | eqid 2824 |
. . . 4
⊢
(𝒫 𝐴 ∩
Fin) = (𝒫 𝐴 ∩
Fin) |
164 | 39, 147, 163, 41, 149, 46, 43 | eltsms 22744 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ (TopOpen‘𝐺)(𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))))) |
165 | 146, 162,
164 | 3bitr4d 313 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums (𝐹 ↾ 𝑊)) ↔ 𝑥 ∈ (𝐺 tsums 𝐹))) |
166 | 165 | eqrdv 2822 |
1
⊢ (𝜑 → (𝐺 tsums (𝐹 ↾ 𝑊)) = (𝐺 tsums 𝐹)) |