Step |
Hyp |
Ref |
Expression |
1 |
|
tsmsres.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
tsmsres.z |
⊢ 0 = ( 0g ‘ 𝐺 ) |
3 |
|
tsmsres.1 |
⊢ ( 𝜑 → 𝐺 ∈ CMnd ) |
4 |
|
tsmsres.2 |
⊢ ( 𝜑 → 𝐺 ∈ TopSp ) |
5 |
|
tsmsres.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
6 |
|
tsmsres.f |
⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 ) |
7 |
|
tsmsres.s |
⊢ ( 𝜑 → ( 𝐹 supp 0 ) ⊆ 𝑊 ) |
8 |
|
inss1 |
⊢ ( 𝐴 ∩ 𝑊 ) ⊆ 𝐴 |
9 |
8
|
sspwi |
⊢ 𝒫 ( 𝐴 ∩ 𝑊 ) ⊆ 𝒫 𝐴 |
10 |
|
ssrin |
⊢ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ⊆ 𝒫 𝐴 → ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ⊆ ( 𝒫 𝐴 ∩ Fin ) ) |
11 |
9 10
|
ax-mp |
⊢ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ⊆ ( 𝒫 𝐴 ∩ Fin ) |
12 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) |
13 |
11 12
|
sseldi |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
14 |
|
elfpw |
⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑧 ⊆ 𝐴 ∧ 𝑧 ∈ Fin ) ) |
15 |
14
|
simplbi |
⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ⊆ 𝐴 ) |
16 |
15
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑧 ⊆ 𝐴 ) |
17 |
16
|
ssrind |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑧 ∩ 𝑊 ) ⊆ ( 𝐴 ∩ 𝑊 ) ) |
18 |
|
elinel2 |
⊢ ( 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑧 ∈ Fin ) |
19 |
18
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑧 ∈ Fin ) |
20 |
|
inss1 |
⊢ ( 𝑧 ∩ 𝑊 ) ⊆ 𝑧 |
21 |
|
ssfi |
⊢ ( ( 𝑧 ∈ Fin ∧ ( 𝑧 ∩ 𝑊 ) ⊆ 𝑧 ) → ( 𝑧 ∩ 𝑊 ) ∈ Fin ) |
22 |
19 20 21
|
sylancl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑧 ∩ 𝑊 ) ∈ Fin ) |
23 |
|
elfpw |
⊢ ( ( 𝑧 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ↔ ( ( 𝑧 ∩ 𝑊 ) ⊆ ( 𝐴 ∩ 𝑊 ) ∧ ( 𝑧 ∩ 𝑊 ) ∈ Fin ) ) |
24 |
17 22 23
|
sylanbrc |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑧 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) |
25 |
|
sseq2 |
⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( 𝑎 ⊆ 𝑏 ↔ 𝑎 ⊆ ( 𝑧 ∩ 𝑊 ) ) ) |
26 |
|
ssin |
⊢ ( ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) ↔ 𝑎 ⊆ ( 𝑧 ∩ 𝑊 ) ) |
27 |
25 26
|
bitr4di |
⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( 𝑎 ⊆ 𝑏 ↔ ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) ) ) |
28 |
|
reseq2 |
⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) = ( ( 𝐹 ↾ 𝑊 ) ↾ ( 𝑧 ∩ 𝑊 ) ) ) |
29 |
|
inss2 |
⊢ ( 𝑧 ∩ 𝑊 ) ⊆ 𝑊 |
30 |
|
resabs1 |
⊢ ( ( 𝑧 ∩ 𝑊 ) ⊆ 𝑊 → ( ( 𝐹 ↾ 𝑊 ) ↾ ( 𝑧 ∩ 𝑊 ) ) = ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) |
31 |
29 30
|
ax-mp |
⊢ ( ( 𝐹 ↾ 𝑊 ) ↾ ( 𝑧 ∩ 𝑊 ) ) = ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) |
32 |
28 31
|
eqtrdi |
⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) = ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) |
33 |
32
|
oveq2d |
⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ) |
34 |
33
|
eleq1d |
⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) ) |
35 |
27 34
|
imbi12d |
⊢ ( 𝑏 = ( 𝑧 ∩ 𝑊 ) → ( ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ↔ ( ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) ) ) |
36 |
35
|
rspcv |
⊢ ( ( 𝑧 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ( ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) ) ) |
37 |
24 36
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ( ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) ) ) |
38 |
|
elfpw |
⊢ ( 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ↔ ( 𝑎 ⊆ ( 𝐴 ∩ 𝑊 ) ∧ 𝑎 ∈ Fin ) ) |
39 |
38
|
simplbi |
⊢ ( 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) → 𝑎 ⊆ ( 𝐴 ∩ 𝑊 ) ) |
40 |
39
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ⊆ ( 𝐴 ∩ 𝑊 ) ) |
41 |
|
inss2 |
⊢ ( 𝐴 ∩ 𝑊 ) ⊆ 𝑊 |
42 |
40 41
|
sstrdi |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ⊆ 𝑊 ) |
43 |
42
|
biantrud |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑎 ⊆ 𝑧 ↔ ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) ) ) |
44 |
|
resres |
⊢ ( ( 𝐹 ↾ 𝑧 ) ↾ 𝑊 ) = ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) |
45 |
44
|
oveq2i |
⊢ ( 𝐺 Σg ( ( 𝐹 ↾ 𝑧 ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) |
46 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐺 ∈ CMnd ) |
47 |
6
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
48 |
47 16
|
fssresd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑧 ) : 𝑧 ⟶ 𝐵 ) |
49 |
|
fex |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ 𝐴 ∈ 𝑉 ) → 𝐹 ∈ V ) |
50 |
6 5 49
|
syl2anc |
⊢ ( 𝜑 → 𝐹 ∈ V ) |
51 |
50
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝐹 ∈ V ) |
52 |
2
|
fvexi |
⊢ 0 ∈ V |
53 |
|
ressuppss |
⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ↾ 𝑧 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) ) |
54 |
51 52 53
|
sylancl |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 ↾ 𝑧 ) supp 0 ) ⊆ ( 𝐹 supp 0 ) ) |
55 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 supp 0 ) ⊆ 𝑊 ) |
56 |
54 55
|
sstrd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐹 ↾ 𝑧 ) supp 0 ) ⊆ 𝑊 ) |
57 |
52
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 0 ∈ V ) |
58 |
48 19 57
|
fdmfifsupp |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐹 ↾ 𝑧 ) finSupp 0 ) |
59 |
1 2 46 19 48 56 58
|
gsumres |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑧 ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ) |
60 |
45 59
|
syl5reqr |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ) |
61 |
60
|
eleq1d |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) ) |
62 |
43 61
|
imbi12d |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( ( 𝑎 ⊆ 𝑧 ∧ 𝑎 ⊆ 𝑊 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑧 ∩ 𝑊 ) ) ) ∈ 𝑢 ) ) ) |
63 |
37 62
|
sylibrd |
⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) ∧ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) |
64 |
63
|
ralrimdva |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) |
65 |
|
sseq1 |
⊢ ( 𝑦 = 𝑎 → ( 𝑦 ⊆ 𝑧 ↔ 𝑎 ⊆ 𝑧 ) ) |
66 |
65
|
rspceaimv |
⊢ ( ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑎 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) |
67 |
13 64 66
|
syl6an |
⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) |
68 |
67
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) |
69 |
|
elfpw |
⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ Fin ) ) |
70 |
69
|
simplbi |
⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ⊆ 𝐴 ) |
71 |
70
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ⊆ 𝐴 ) |
72 |
71
|
ssrind |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∩ 𝑊 ) ⊆ ( 𝐴 ∩ 𝑊 ) ) |
73 |
|
elinel2 |
⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ Fin ) |
74 |
73
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ Fin ) |
75 |
|
inss1 |
⊢ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑦 |
76 |
|
ssfi |
⊢ ( ( 𝑦 ∈ Fin ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑦 ) → ( 𝑦 ∩ 𝑊 ) ∈ Fin ) |
77 |
74 75 76
|
sylancl |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∩ 𝑊 ) ∈ Fin ) |
78 |
|
elfpw |
⊢ ( ( 𝑦 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ↔ ( ( 𝑦 ∩ 𝑊 ) ⊆ ( 𝐴 ∩ 𝑊 ) ∧ ( 𝑦 ∩ 𝑊 ) ∈ Fin ) ) |
79 |
72 77 78
|
sylanbrc |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝑦 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) |
80 |
70
|
ad2antlr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑦 ⊆ 𝐴 ) |
81 |
|
elfpw |
⊢ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ↔ ( 𝑏 ⊆ ( 𝐴 ∩ 𝑊 ) ∧ 𝑏 ∈ Fin ) ) |
82 |
81
|
simplbi |
⊢ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) → 𝑏 ⊆ ( 𝐴 ∩ 𝑊 ) ) |
83 |
82
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑏 ⊆ ( 𝐴 ∩ 𝑊 ) ) |
84 |
83 8
|
sstrdi |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑏 ⊆ 𝐴 ) |
85 |
80 84
|
unssd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( 𝑦 ∪ 𝑏 ) ⊆ 𝐴 ) |
86 |
|
elinel2 |
⊢ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) → 𝑏 ∈ Fin ) |
87 |
|
unfi |
⊢ ( ( 𝑦 ∈ Fin ∧ 𝑏 ∈ Fin ) → ( 𝑦 ∪ 𝑏 ) ∈ Fin ) |
88 |
74 86 87
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( 𝑦 ∪ 𝑏 ) ∈ Fin ) |
89 |
|
elfpw |
⊢ ( ( 𝑦 ∪ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ( 𝑦 ∪ 𝑏 ) ⊆ 𝐴 ∧ ( 𝑦 ∪ 𝑏 ) ∈ Fin ) ) |
90 |
85 88 89
|
sylanbrc |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( 𝑦 ∪ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) ) |
91 |
|
ssun1 |
⊢ 𝑦 ⊆ ( 𝑦 ∪ 𝑏 ) |
92 |
|
id |
⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → 𝑧 = ( 𝑦 ∪ 𝑏 ) ) |
93 |
91 92
|
sseqtrrid |
⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → 𝑦 ⊆ 𝑧 ) |
94 |
|
pm5.5 |
⊢ ( 𝑦 ⊆ 𝑧 → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) |
95 |
93 94
|
syl |
⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) |
96 |
|
reseq2 |
⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( 𝐹 ↾ 𝑧 ) = ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) |
97 |
96
|
oveq2d |
⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ) |
98 |
97
|
eleq1d |
⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) ) |
99 |
95 98
|
bitrd |
⊢ ( 𝑧 = ( 𝑦 ∪ 𝑏 ) → ( ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ↔ ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) ) |
100 |
99
|
rspcv |
⊢ ( ( 𝑦 ∪ 𝑏 ) ∈ ( 𝒫 𝐴 ∩ Fin ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) ) |
101 |
90 100
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ) ) |
102 |
3
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 𝐺 ∈ CMnd ) |
103 |
88
|
adantrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑦 ∪ 𝑏 ) ∈ Fin ) |
104 |
6
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 𝐹 : 𝐴 ⟶ 𝐵 ) |
105 |
85
|
adantrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑦 ∪ 𝑏 ) ⊆ 𝐴 ) |
106 |
104 105
|
fssresd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) : ( 𝑦 ∪ 𝑏 ) ⟶ 𝐵 ) |
107 |
50 52
|
jctir |
⊢ ( 𝜑 → ( 𝐹 ∈ V ∧ 0 ∈ V ) ) |
108 |
107
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ∈ V ∧ 0 ∈ V ) ) |
109 |
|
ressuppss |
⊢ ( ( 𝐹 ∈ V ∧ 0 ∈ V ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) ) |
110 |
108 109
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) supp 0 ) ⊆ ( 𝐹 supp 0 ) ) |
111 |
7
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 supp 0 ) ⊆ 𝑊 ) |
112 |
110 111
|
sstrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) supp 0 ) ⊆ 𝑊 ) |
113 |
52
|
a1i |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 0 ∈ V ) |
114 |
106 103 113
|
fdmfifsupp |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) finSupp 0 ) |
115 |
1 2 102 103 106 112 114
|
gsumres |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ) |
116 |
|
resres |
⊢ ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) = ( 𝐹 ↾ ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) ) |
117 |
|
indir |
⊢ ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) = ( ( 𝑦 ∩ 𝑊 ) ∪ ( 𝑏 ∩ 𝑊 ) ) |
118 |
83 41
|
sstrdi |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → 𝑏 ⊆ 𝑊 ) |
119 |
118
|
adantrr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → 𝑏 ⊆ 𝑊 ) |
120 |
|
df-ss |
⊢ ( 𝑏 ⊆ 𝑊 ↔ ( 𝑏 ∩ 𝑊 ) = 𝑏 ) |
121 |
119 120
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑏 ∩ 𝑊 ) = 𝑏 ) |
122 |
121
|
uneq2d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∩ 𝑊 ) ∪ ( 𝑏 ∩ 𝑊 ) ) = ( ( 𝑦 ∩ 𝑊 ) ∪ 𝑏 ) ) |
123 |
|
simprr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) |
124 |
|
ssequn1 |
⊢ ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ↔ ( ( 𝑦 ∩ 𝑊 ) ∪ 𝑏 ) = 𝑏 ) |
125 |
123 124
|
sylib |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∩ 𝑊 ) ∪ 𝑏 ) = 𝑏 ) |
126 |
122 125
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∩ 𝑊 ) ∪ ( 𝑏 ∩ 𝑊 ) ) = 𝑏 ) |
127 |
117 126
|
syl5eq |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) = 𝑏 ) |
128 |
127
|
reseq2d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐹 ↾ ( ( 𝑦 ∪ 𝑏 ) ∩ 𝑊 ) ) = ( 𝐹 ↾ 𝑏 ) ) |
129 |
116 128
|
syl5eq |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) = ( 𝐹 ↾ 𝑏 ) ) |
130 |
119
|
resabs1d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) = ( 𝐹 ↾ 𝑏 ) ) |
131 |
129 130
|
eqtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) = ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) |
132 |
131
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐺 Σg ( ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ↾ 𝑊 ) ) = ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ) |
133 |
115 132
|
eqtr3d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) = ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ) |
134 |
133
|
eleq1d |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 ↔ ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) |
135 |
134
|
biimpd |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) |
136 |
135
|
expr |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) |
137 |
136
|
com23 |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ( 𝐺 Σg ( 𝐹 ↾ ( 𝑦 ∪ 𝑏 ) ) ) ∈ 𝑢 → ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) |
138 |
101 137
|
syld |
⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) |
139 |
138
|
ralrimdva |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) |
140 |
|
sseq1 |
⊢ ( 𝑎 = ( 𝑦 ∩ 𝑊 ) → ( 𝑎 ⊆ 𝑏 ↔ ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 ) ) |
141 |
140
|
rspceaimv |
⊢ ( ( ( 𝑦 ∩ 𝑊 ) ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∧ ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( ( 𝑦 ∩ 𝑊 ) ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) |
142 |
79 139 141
|
syl6an |
⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) |
143 |
142
|
rexlimdva |
⊢ ( 𝜑 → ( ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) |
144 |
68 143
|
impbid |
⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ↔ ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) |
145 |
144
|
imbi2d |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ↔ ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ) |
146 |
145
|
ralbidv |
⊢ ( 𝜑 → ( ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ↔ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ) |
147 |
146
|
anbi2d |
⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ) ) |
148 |
|
eqid |
⊢ ( TopOpen ‘ 𝐺 ) = ( TopOpen ‘ 𝐺 ) |
149 |
|
eqid |
⊢ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) = ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) |
150 |
|
inex1g |
⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∩ 𝑊 ) ∈ V ) |
151 |
5 150
|
syl |
⊢ ( 𝜑 → ( 𝐴 ∩ 𝑊 ) ∈ V ) |
152 |
|
fssres |
⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ( 𝐴 ∩ 𝑊 ) ⊆ 𝐴 ) → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ) |
153 |
6 8 152
|
sylancl |
⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ) |
154 |
|
resres |
⊢ ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑊 ) = ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) |
155 |
|
ffn |
⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 ) |
156 |
|
fnresdm |
⊢ ( 𝐹 Fn 𝐴 → ( 𝐹 ↾ 𝐴 ) = 𝐹 ) |
157 |
6 155 156
|
3syl |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝐴 ) = 𝐹 ) |
158 |
157
|
reseq1d |
⊢ ( 𝜑 → ( ( 𝐹 ↾ 𝐴 ) ↾ 𝑊 ) = ( 𝐹 ↾ 𝑊 ) ) |
159 |
154 158
|
syl5eqr |
⊢ ( 𝜑 → ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) = ( 𝐹 ↾ 𝑊 ) ) |
160 |
159
|
feq1d |
⊢ ( 𝜑 → ( ( 𝐹 ↾ ( 𝐴 ∩ 𝑊 ) ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ↔ ( 𝐹 ↾ 𝑊 ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ) ) |
161 |
153 160
|
mpbid |
⊢ ( 𝜑 → ( 𝐹 ↾ 𝑊 ) : ( 𝐴 ∩ 𝑊 ) ⟶ 𝐵 ) |
162 |
1 148 149 3 4 151 161
|
eltsms |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums ( 𝐹 ↾ 𝑊 ) ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑎 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ∀ 𝑏 ∈ ( 𝒫 ( 𝐴 ∩ 𝑊 ) ∩ Fin ) ( 𝑎 ⊆ 𝑏 → ( 𝐺 Σg ( ( 𝐹 ↾ 𝑊 ) ↾ 𝑏 ) ) ∈ 𝑢 ) ) ) ) ) |
163 |
|
eqid |
⊢ ( 𝒫 𝐴 ∩ Fin ) = ( 𝒫 𝐴 ∩ Fin ) |
164 |
1 148 163 3 4 5 6
|
eltsms |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ↔ ( 𝑥 ∈ 𝐵 ∧ ∀ 𝑢 ∈ ( TopOpen ‘ 𝐺 ) ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ∀ 𝑧 ∈ ( 𝒫 𝐴 ∩ Fin ) ( 𝑦 ⊆ 𝑧 → ( 𝐺 Σg ( 𝐹 ↾ 𝑧 ) ) ∈ 𝑢 ) ) ) ) ) |
165 |
147 162 164
|
3bitr4d |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 𝐺 tsums ( 𝐹 ↾ 𝑊 ) ) ↔ 𝑥 ∈ ( 𝐺 tsums 𝐹 ) ) ) |
166 |
165
|
eqrdv |
⊢ ( 𝜑 → ( 𝐺 tsums ( 𝐹 ↾ 𝑊 ) ) = ( 𝐺 tsums 𝐹 ) ) |