Metamath Proof Explorer

Theorem eltsms

Description: The property of being a sum of the sequence F in the topological commutative monoid G . (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypotheses eltsms.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
eltsms.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
eltsms.s ⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
eltsms.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
eltsms.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
eltsms.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
eltsms.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
Assertion eltsms ( 𝜑 → ( 𝐶 ∈ ( 𝐺 tsums 𝐹 ) ↔ ( 𝐶 ∈ 𝐵 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝐶 ∈ 𝑢 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 eltsms.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 eltsms.j ⊢ 𝐽 = ( TopOpen ‘ 𝐺 )
3 eltsms.s ⊢ 𝑆 = ( 𝒫 𝐴 ∩ Fin )
4 eltsms.1 ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
5 eltsms.2 ⊢ ( 𝜑 → 𝐺 ∈ TopSp )
6 eltsms.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
7 eltsms.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐵 )
8 eqid ⊢ ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) = ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
9 1 2 3 8 4 6 7 tsmsval ⊢ ( 𝜑 → ( 𝐺 tsums 𝐹 ) = ( ( 𝐽 fLimf ( 𝑆 filGen ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) )
10 9 eleq2d ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐺 tsums 𝐹 ) ↔ 𝐶 ∈ ( ( 𝐽 fLimf ( 𝑆 filGen ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) ) )
11 1 2 istps ⊢ ( 𝐺 ∈ TopSp ↔ 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
12 5 11 sylib ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝐵 ) )
13 eqid ⊢ ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) = ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } )
14 3 13 8 6 tsmsfbas ⊢ ( 𝜑 → ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ∈ ( fBas ‘ 𝑆 ) )
15 1 3 4 6 7 tsmslem1 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝐵 )
16 15 fmpttd ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) : 𝑆 ⟶ 𝐵 )
17 eqid ⊢ ( 𝑆 filGen ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ) = ( 𝑆 filGen ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) )
18 17 flffbas ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝐵 ) ∧ ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ∈ ( fBas ‘ 𝑆 ) ∧ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) : 𝑆 ⟶ 𝐵 ) → ( 𝐶 ∈ ( ( 𝐽 fLimf ( 𝑆 filGen ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) ↔ ( 𝐶 ∈ 𝐵 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑤 ) ⊆ 𝑢 ) ) ) )
19 12 14 16 18 syl3anc ⊢ ( 𝜑 → ( 𝐶 ∈ ( ( 𝐽 fLimf ( 𝑆 filGen ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ) ) ‘ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) ↔ ( 𝐶 ∈ 𝐵 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑤 ) ⊆ 𝑢 ) ) ) )
20 pwexg ⊢ ( 𝐴 ∈ 𝑉 → 𝒫 𝐴 ∈ V )
21 inex1g ⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∩ Fin ) ∈ V )
22 6 20 21 3syl ⊢ ( 𝜑 → ( 𝒫 𝐴 ∩ Fin ) ∈ V )
23 3 22 eqeltrid ⊢ ( 𝜑 → 𝑆 ∈ V )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → 𝑆 ∈ V )
25 rabexg ⊢ ( 𝑆 ∈ V → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ∈ V )
26 24 25 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ∈ V )
27 26 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ∀ 𝑧 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ∈ V )
28 imaeq2 ⊢ ( 𝑤 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } → ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑤 ) = ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) )
29 28 sseq1d ⊢ ( 𝑤 = { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } → ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑤 ) ⊆ 𝑢 ↔ ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ⊆ 𝑢 ) )
30 13 29 rexrnmptw ⊢ ( ∀ 𝑧 ∈ 𝑆 { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ∈ V → ( ∃ 𝑤 ∈ ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑤 ) ⊆ 𝑢 ↔ ∃ 𝑧 ∈ 𝑆 ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ⊆ 𝑢 ) )
31 27 30 syl ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ( ∃ 𝑤 ∈ ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑤 ) ⊆ 𝑢 ↔ ∃ 𝑧 ∈ 𝑆 ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ⊆ 𝑢 ) )
32 funmpt ⊢ Fun ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) )
33 ssrab2 ⊢ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ 𝑆
34 ovex ⊢ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ V
35 eqid ⊢ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) = ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) )
36 34 35 dmmpti ⊢ dom ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) = 𝑆
37 33 36 sseqtrri ⊢ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ dom ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) )
38 funimass3 ⊢ ( ( Fun ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ∧ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ dom ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) ) → ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ⊆ 𝑢 ↔ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ ( ◡ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑢 ) ) )
39 32 37 38 mp2an ⊢ ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ⊆ 𝑢 ↔ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ ( ◡ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑢 ) )
40 35 mptpreima ⊢ ( ◡ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑢 ) = { 𝑦 ∈ 𝑆 ∣ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 }
41 40 sseq2i ⊢ ( { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ ( ◡ ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑢 ) ↔ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ { 𝑦 ∈ 𝑆 ∣ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 } )
42 ss2rab ⊢ ( { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ⊆ { 𝑦 ∈ 𝑆 ∣ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 } ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) )
43 39 41 42 3bitri ⊢ ( ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ⊆ 𝑢 ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) )
44 43 rexbii ⊢ ( ∃ 𝑧 ∈ 𝑆 ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ⊆ 𝑢 ↔ ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) )
45 31 44 bitrdi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ( ∃ 𝑤 ∈ ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑤 ) ⊆ 𝑢 ↔ ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) )
46 45 imbi2d ⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝐽 ) → ( ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑤 ) ⊆ 𝑢 ) ↔ ( 𝐶 ∈ 𝑢 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) )
47 46 ralbidva ⊢ ( 𝜑 → ( ∀ 𝑢 ∈ 𝐽 ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑤 ) ⊆ 𝑢 ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝐶 ∈ 𝑢 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) )
48 47 anbi2d ⊢ ( 𝜑 → ( ( 𝐶 ∈ 𝐵 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝐶 ∈ 𝑢 → ∃ 𝑤 ∈ ran ( 𝑧 ∈ 𝑆 ↦ { 𝑦 ∈ 𝑆 ∣ 𝑧 ⊆ 𝑦 } ) ( ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ) “ 𝑤 ) ⊆ 𝑢 ) ) ↔ ( 𝐶 ∈ 𝐵 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝐶 ∈ 𝑢 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) ) )
49 10 19 48 3bitrd ⊢ ( 𝜑 → ( 𝐶 ∈ ( 𝐺 tsums 𝐹 ) ↔ ( 𝐶 ∈ 𝐵 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝐶 ∈ 𝑢 → ∃ 𝑧 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑧 ⊆ 𝑦 → ( 𝐺 Σg ( 𝐹 ↾ 𝑦 ) ) ∈ 𝑢 ) ) ) ) )