Step | Hyp | Ref
| Expression |
1 | | tsmsid.2 |
. . . . . . 7
⊢ (𝜑 → 𝐺 ∈ TopSp) |
2 | | tsmsid.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝐺) |
3 | | tsmsgsum.j |
. . . . . . . 8
⊢ 𝐽 = (TopOpen‘𝐺) |
4 | 2, 3 | istps 21831 |
. . . . . . 7
⊢ (𝐺 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐵)) |
5 | 1, 4 | sylib 221 |
. . . . . 6
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝐵)) |
6 | | toponuni 21811 |
. . . . . 6
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) |
7 | 5, 6 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐵 = ∪ 𝐽) |
8 | 7 | eleq2d 2823 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↔ 𝑥 ∈ ∪ 𝐽)) |
9 | | elfpw 8978 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) ↔ (𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin)) |
10 | 9 | simplbi 501 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ⊆ 𝐴) |
11 | 10 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ⊆ 𝐴) |
12 | | suppssdm 7919 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 supp 0 ) ⊆ dom 𝐹 |
13 | | tsmsid.f |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹:𝐴⟶𝐵) |
14 | 12, 13 | fssdm 6565 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝐹 supp 0 ) ⊆ 𝐴) |
15 | 14 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 supp 0 ) ⊆ 𝐴) |
16 | 11, 15 | unssd 4100 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑦 ∪ (𝐹 supp 0 )) ⊆ 𝐴) |
17 | | elinel2 4110 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ Fin) |
18 | 17 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin) |
19 | | tsmsid.w |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐹 finSupp 0 ) |
20 | 19 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹 finSupp 0 ) |
21 | 20 | fsuppimpd 8992 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 supp 0 ) ∈
Fin) |
22 | | unfi 8850 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∈ Fin ∧ (𝐹 supp 0 ) ∈ Fin) →
(𝑦 ∪ (𝐹 supp 0 )) ∈
Fin) |
23 | 18, 21, 22 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑦 ∪ (𝐹 supp 0 )) ∈
Fin) |
24 | | elfpw 8978 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∪ (𝐹 supp 0 )) ∈ (𝒫 𝐴 ∩ Fin) ↔ ((𝑦 ∪ (𝐹 supp 0 )) ⊆ 𝐴 ∧ (𝑦 ∪ (𝐹 supp 0 )) ∈
Fin)) |
25 | 16, 23, 24 | sylanbrc 586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝑦 ∪ (𝐹 supp 0 )) ∈ (𝒫 𝐴 ∩ Fin)) |
26 | | ssun1 4086 |
. . . . . . . . . . . . . . 15
⊢ 𝑦 ⊆ (𝑦 ∪ (𝐹 supp 0 )) |
27 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 ∪ (𝐹 supp 0 )) → 𝑧 = (𝑦 ∪ (𝐹 supp 0 ))) |
28 | 26, 27 | sseqtrrid 3954 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦 ∪ (𝐹 supp 0 )) → 𝑦 ⊆ 𝑧) |
29 | | pm5.5 365 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ⊆ 𝑧 → ((𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑦 ∪ (𝐹 supp 0 )) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
31 | | reseq2 5846 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 ∪ (𝐹 supp 0 )) → (𝐹 ↾ 𝑧) = (𝐹 ↾ (𝑦 ∪ (𝐹 supp 0 )))) |
32 | 31 | oveq2d 7229 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦 ∪ (𝐹 supp 0 )) → (𝐺 Σg
(𝐹 ↾ 𝑧)) = (𝐺 Σg (𝐹 ↾ (𝑦 ∪ (𝐹 supp 0 ))))) |
33 | 32 | eleq1d 2822 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑦 ∪ (𝐹 supp 0 )) → ((𝐺 Σg
(𝐹 ↾ 𝑧)) ∈ 𝑢 ↔ (𝐺 Σg (𝐹 ↾ (𝑦 ∪ (𝐹 supp 0 )))) ∈ 𝑢)) |
34 | 30, 33 | bitrd 282 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑦 ∪ (𝐹 supp 0 )) → ((𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝐺 Σg (𝐹 ↾ (𝑦 ∪ (𝐹 supp 0 )))) ∈ 𝑢)) |
35 | 34 | rspcv 3532 |
. . . . . . . . . . 11
⊢ ((𝑦 ∪ (𝐹 supp 0 )) ∈ (𝒫 𝐴 ∩ Fin) →
(∀𝑧 ∈
(𝒫 𝐴 ∩
Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → (𝐺 Σg (𝐹 ↾ (𝑦 ∪ (𝐹 supp 0 )))) ∈ 𝑢)) |
36 | 25, 35 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → (𝐺 Σg (𝐹 ↾ (𝑦 ∪ (𝐹 supp 0 )))) ∈ 𝑢)) |
37 | | tsmsid.z |
. . . . . . . . . . . 12
⊢ 0 =
(0g‘𝐺) |
38 | | tsmsid.1 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐺 ∈ CMnd) |
39 | 38 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐺 ∈ CMnd) |
40 | | tsmsid.a |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ 𝑉) |
41 | 40 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐴 ∈ 𝑉) |
42 | 13 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝐹:𝐴⟶𝐵) |
43 | | ssun2 4087 |
. . . . . . . . . . . . 13
⊢ (𝐹 supp 0 ) ⊆ (𝑦 ∪ (𝐹 supp 0 )) |
44 | 43 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐹 supp 0 ) ⊆ (𝑦 ∪ (𝐹 supp 0 ))) |
45 | 2, 37, 39, 41, 42, 44, 20 | gsumres 19298 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (𝐺 Σg (𝐹 ↾ (𝑦 ∪ (𝐹 supp 0 )))) = (𝐺 Σg 𝐹)) |
46 | 45 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐺 Σg (𝐹 ↾ (𝑦 ∪ (𝐹 supp 0 )))) ∈ 𝑢 ↔ (𝐺 Σg 𝐹) ∈ 𝑢)) |
47 | 36, 46 | sylibd 242 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑢 ∈ 𝐽) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → (∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → (𝐺 Σg 𝐹) ∈ 𝑢)) |
48 | 47 | rexlimdva 3203 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐽) → (∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) → (𝐺 Σg 𝐹) ∈ 𝑢)) |
49 | 19 | fsuppimpd 8992 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝐹 supp 0 ) ∈
Fin) |
50 | | elfpw 8978 |
. . . . . . . . . . 11
⊢ ((𝐹 supp 0 ) ∈ (𝒫 𝐴 ∩ Fin) ↔ ((𝐹 supp 0 ) ⊆ 𝐴 ∧ (𝐹 supp 0 ) ∈
Fin)) |
51 | 14, 49, 50 | sylanbrc 586 |
. . . . . . . . . 10
⊢ (𝜑 → (𝐹 supp 0 ) ∈ (𝒫 𝐴 ∩ Fin)) |
52 | 38 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ (𝐺 Σg 𝐹) ∈ 𝑢)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐹 supp 0 ) ⊆ 𝑧)) → 𝐺 ∈ CMnd) |
53 | 40 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ (𝐺 Σg 𝐹) ∈ 𝑢)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐹 supp 0 ) ⊆ 𝑧)) → 𝐴 ∈ 𝑉) |
54 | 13 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ (𝐺 Σg 𝐹) ∈ 𝑢)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐹 supp 0 ) ⊆ 𝑧)) → 𝐹:𝐴⟶𝐵) |
55 | | simprr 773 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ (𝐺 Σg 𝐹) ∈ 𝑢)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐹 supp 0 ) ⊆ 𝑧)) → (𝐹 supp 0 ) ⊆ 𝑧) |
56 | 19 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ (𝐺 Σg 𝐹) ∈ 𝑢)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐹 supp 0 ) ⊆ 𝑧)) → 𝐹 finSupp 0 ) |
57 | 2, 37, 52, 53, 54, 55, 56 | gsumres 19298 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ (𝐺 Σg 𝐹) ∈ 𝑢)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐹 supp 0 ) ⊆ 𝑧)) → (𝐺 Σg (𝐹 ↾ 𝑧)) = (𝐺 Σg 𝐹)) |
58 | | simplrr 778 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ (𝐺 Σg 𝐹) ∈ 𝑢)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐹 supp 0 ) ⊆ 𝑧)) → (𝐺 Σg 𝐹) ∈ 𝑢) |
59 | 57, 58 | eqeltrd 2838 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ (𝐺 Σg 𝐹) ∈ 𝑢)) ∧ (𝑧 ∈ (𝒫 𝐴 ∩ Fin) ∧ (𝐹 supp 0 ) ⊆ 𝑧)) → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) |
60 | 59 | expr 460 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ (𝐺 Σg 𝐹) ∈ 𝑢)) ∧ 𝑧 ∈ (𝒫 𝐴 ∩ Fin)) → ((𝐹 supp 0 ) ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
61 | 60 | ralrimiva 3105 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ (𝐺 Σg 𝐹) ∈ 𝑢)) → ∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)((𝐹 supp 0 ) ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
62 | | sseq1 3926 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹 supp 0 ) → (𝑦 ⊆ 𝑧 ↔ (𝐹 supp 0 ) ⊆ 𝑧)) |
63 | 62 | rspceaimv 3542 |
. . . . . . . . . 10
⊢ (((𝐹 supp 0 ) ∈ (𝒫 𝐴 ∩ Fin) ∧ ∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)((𝐹 supp 0 ) ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
64 | 51, 61, 63 | syl2an2r 685 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑢 ∈ 𝐽 ∧ (𝐺 Σg 𝐹) ∈ 𝑢)) → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) |
65 | 64 | expr 460 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐽) → ((𝐺 Σg 𝐹) ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) |
66 | 48, 65 | impbid 215 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐽) → (∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝐺 Σg 𝐹) ∈ 𝑢)) |
67 | | disjsn 4627 |
. . . . . . . 8
⊢ ((𝑢 ∩ {(𝐺 Σg 𝐹)}) = ∅ ↔ ¬
(𝐺
Σg 𝐹) ∈ 𝑢) |
68 | 67 | necon2abii 2991 |
. . . . . . 7
⊢ ((𝐺 Σg
𝐹) ∈ 𝑢 ↔ (𝑢 ∩ {(𝐺 Σg 𝐹)}) ≠
∅) |
69 | 66, 68 | bitrdi 290 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐽) → (∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢) ↔ (𝑢 ∩ {(𝐺 Σg 𝐹)}) ≠
∅)) |
70 | 69 | imbi2d 344 |
. . . . 5
⊢ ((𝜑 ∧ 𝑢 ∈ 𝐽) → ((𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) ↔ (𝑥 ∈ 𝑢 → (𝑢 ∩ {(𝐺 Σg 𝐹)}) ≠
∅))) |
71 | 70 | ralbidva 3117 |
. . . 4
⊢ (𝜑 → (∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢)) ↔ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → (𝑢 ∩ {(𝐺 Σg 𝐹)}) ≠
∅))) |
72 | 8, 71 | anbi12d 634 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))) ↔ (𝑥 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → (𝑢 ∩ {(𝐺 Σg 𝐹)}) ≠
∅)))) |
73 | | eqid 2737 |
. . . 4
⊢
(𝒫 𝐴 ∩
Fin) = (𝒫 𝐴 ∩
Fin) |
74 | 2, 3, 73, 38, 1, 40, 13 | eltsms 23030 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ (𝑥 ∈ 𝐵 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → ∃𝑦 ∈ (𝒫 𝐴 ∩ Fin)∀𝑧 ∈ (𝒫 𝐴 ∩ Fin)(𝑦 ⊆ 𝑧 → (𝐺 Σg (𝐹 ↾ 𝑧)) ∈ 𝑢))))) |
75 | | topontop 21810 |
. . . . 5
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) |
76 | 5, 75 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐽 ∈ Top) |
77 | 2, 37, 38, 40, 13, 19 | gsumcl 19300 |
. . . . . 6
⊢ (𝜑 → (𝐺 Σg 𝐹) ∈ 𝐵) |
78 | 77 | snssd 4722 |
. . . . 5
⊢ (𝜑 → {(𝐺 Σg 𝐹)} ⊆ 𝐵) |
79 | 78, 7 | sseqtrd 3941 |
. . . 4
⊢ (𝜑 → {(𝐺 Σg 𝐹)} ⊆ ∪ 𝐽) |
80 | | eqid 2737 |
. . . . 5
⊢ ∪ 𝐽 =
∪ 𝐽 |
81 | 80 | elcls2 21971 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ {(𝐺 Σg
𝐹)} ⊆ ∪ 𝐽)
→ (𝑥 ∈
((cls‘𝐽)‘{(𝐺 Σg 𝐹)}) ↔ (𝑥 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → (𝑢 ∩ {(𝐺 Σg 𝐹)}) ≠
∅)))) |
82 | 76, 79, 81 | syl2anc 587 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((cls‘𝐽)‘{(𝐺 Σg 𝐹)}) ↔ (𝑥 ∈ ∪ 𝐽 ∧ ∀𝑢 ∈ 𝐽 (𝑥 ∈ 𝑢 → (𝑢 ∩ {(𝐺 Σg 𝐹)}) ≠
∅)))) |
83 | 72, 74, 82 | 3bitr4d 314 |
. 2
⊢ (𝜑 → (𝑥 ∈ (𝐺 tsums 𝐹) ↔ 𝑥 ∈ ((cls‘𝐽)‘{(𝐺 Σg 𝐹)}))) |
84 | 83 | eqrdv 2735 |
1
⊢ (𝜑 → (𝐺 tsums 𝐹) = ((cls‘𝐽)‘{(𝐺 Σg 𝐹)})) |