Proof of Theorem sitgclg
Step | Hyp | Ref
| Expression |
1 | | sitgval.b |
. . 3
⊢ 𝐵 = (Base‘𝑊) |
2 | | sitgval.j |
. . 3
⊢ 𝐽 = (TopOpen‘𝑊) |
3 | | sitgval.s |
. . 3
⊢ 𝑆 = (sigaGen‘𝐽) |
4 | | sitgval.0 |
. . 3
⊢ 0 =
(0g‘𝑊) |
5 | | sitgval.x |
. . 3
⊢ · = (
·𝑠 ‘𝑊) |
6 | | sitgval.h |
. . 3
⊢ 𝐻 =
(ℝHom‘(Scalar‘𝑊)) |
7 | | sitgval.1 |
. . 3
⊢ (𝜑 → 𝑊 ∈ 𝑉) |
8 | | sitgval.2 |
. . 3
⊢ (𝜑 → 𝑀 ∈ ∪ ran
measures) |
9 | | sibfmbl.1 |
. . 3
⊢ (𝜑 → 𝐹 ∈ dom (𝑊sitg𝑀)) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | sitgfval 32020 |
. 2
⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) = (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)))) |
11 | | sitgclg.2 |
. . 3
⊢ (𝜑 → 𝑊 ∈ CMnd) |
12 | | rnexg 7682 |
. . . 4
⊢ (𝐹 ∈ dom (𝑊sitg𝑀) → ran 𝐹 ∈ V) |
13 | | difexg 5220 |
. . . 4
⊢ (ran
𝐹 ∈ V → (ran
𝐹 ∖ { 0 }) ∈
V) |
14 | 9, 12, 13 | 3syl 18 |
. . 3
⊢ (𝜑 → (ran 𝐹 ∖ { 0 }) ∈
V) |
15 | | simpl 486 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝜑) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | sibfima 32017 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → (𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞)) |
17 | | sitgclg.d |
. . . . . . . . . . 11
⊢ 𝐷 = ((dist‘𝐺) ↾ ((Base‘𝐺) × (Base‘𝐺))) |
18 | | sitgclg.g |
. . . . . . . . . . . . 13
⊢ 𝐺 = (Scalar‘𝑊) |
19 | 18 | fveq2i 6720 |
. . . . . . . . . . . 12
⊢
(dist‘𝐺) =
(dist‘(Scalar‘𝑊)) |
20 | 18 | fveq2i 6720 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺) =
(Base‘(Scalar‘𝑊)) |
21 | 20, 20 | xpeq12i 5579 |
. . . . . . . . . . . 12
⊢
((Base‘𝐺)
× (Base‘𝐺)) =
((Base‘(Scalar‘𝑊)) × (Base‘(Scalar‘𝑊))) |
22 | 19, 21 | reseq12i 5849 |
. . . . . . . . . . 11
⊢
((dist‘𝐺)
↾ ((Base‘𝐺)
× (Base‘𝐺))) =
((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) ×
(Base‘(Scalar‘𝑊)))) |
23 | 17, 22 | eqtri 2765 |
. . . . . . . . . 10
⊢ 𝐷 =
((dist‘(Scalar‘𝑊)) ↾ ((Base‘(Scalar‘𝑊)) ×
(Base‘(Scalar‘𝑊)))) |
24 | | eqid 2737 |
. . . . . . . . . 10
⊢
(topGen‘ran (,)) = (topGen‘ran (,)) |
25 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
26 | 18 | fveq2i 6720 |
. . . . . . . . . 10
⊢
(TopOpen‘𝐺) =
(TopOpen‘(Scalar‘𝑊)) |
27 | 18 | fveq2i 6720 |
. . . . . . . . . 10
⊢
(ℤMod‘𝐺)
= (ℤMod‘(Scalar‘𝑊)) |
28 | | sitgclg.3 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (Scalar‘𝑊) ∈ ℝExt
) |
29 | 18, 28 | eqeltrid 2842 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐺 ∈ ℝExt ) |
30 | | rrextdrg 31664 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt → 𝐺 ∈
DivRing) |
31 | 29, 30 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ DivRing) |
32 | 18, 31 | eqeltrrid 2843 |
. . . . . . . . . 10
⊢ (𝜑 → (Scalar‘𝑊) ∈
DivRing) |
33 | | rrextnrg 31663 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt → 𝐺 ∈
NrmRing) |
34 | 29, 33 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ NrmRing) |
35 | 18, 34 | eqeltrrid 2843 |
. . . . . . . . . 10
⊢ (𝜑 → (Scalar‘𝑊) ∈
NrmRing) |
36 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(ℤMod‘𝐺)
= (ℤMod‘𝐺) |
37 | 36 | rrextnlm 31665 |
. . . . . . . . . . 11
⊢ (𝐺 ∈ ℝExt →
(ℤMod‘𝐺) ∈
NrmMod) |
38 | 29, 37 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (ℤMod‘𝐺) ∈
NrmMod) |
39 | 18 | fveq2i 6720 |
. . . . . . . . . . 11
⊢
(chr‘𝐺) =
(chr‘(Scalar‘𝑊)) |
40 | | rrextchr 31666 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt →
(chr‘𝐺) =
0) |
41 | 29, 40 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (chr‘𝐺) = 0) |
42 | 39, 41 | eqtr3id 2792 |
. . . . . . . . . 10
⊢ (𝜑 →
(chr‘(Scalar‘𝑊)) = 0) |
43 | | rrextcusp 31667 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt → 𝐺 ∈
CUnifSp) |
44 | 29, 43 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐺 ∈ CUnifSp) |
45 | 18, 44 | eqeltrrid 2843 |
. . . . . . . . . 10
⊢ (𝜑 → (Scalar‘𝑊) ∈
CUnifSp) |
46 | 18 | fveq2i 6720 |
. . . . . . . . . . 11
⊢
(UnifSt‘𝐺) =
(UnifSt‘(Scalar‘𝑊)) |
47 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝐺) =
(Base‘𝐺) |
48 | 47, 17 | rrextust 31670 |
. . . . . . . . . . . 12
⊢ (𝐺 ∈ ℝExt →
(UnifSt‘𝐺) =
(metUnif‘𝐷)) |
49 | 29, 48 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → (UnifSt‘𝐺) = (metUnif‘𝐷)) |
50 | 46, 49 | eqtr3id 2792 |
. . . . . . . . . 10
⊢ (𝜑 →
(UnifSt‘(Scalar‘𝑊)) = (metUnif‘𝐷)) |
51 | 23, 24, 25, 26, 27, 32, 35, 38, 42, 45, 50 | rrhf 31660 |
. . . . . . . . 9
⊢ (𝜑 →
(ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊))) |
52 | 6 | feq1i 6536 |
. . . . . . . . 9
⊢ (𝐻:ℝ⟶(Base‘(Scalar‘𝑊)) ↔
(ℝHom‘(Scalar‘𝑊)):ℝ⟶(Base‘(Scalar‘𝑊))) |
53 | 51, 52 | sylibr 237 |
. . . . . . . 8
⊢ (𝜑 → 𝐻:ℝ⟶(Base‘(Scalar‘𝑊))) |
54 | 53 | ffund 6549 |
. . . . . . 7
⊢ (𝜑 → Fun 𝐻) |
55 | | rge0ssre 13044 |
. . . . . . . 8
⊢
(0[,)+∞) ⊆ ℝ |
56 | 53 | fdmd 6556 |
. . . . . . . 8
⊢ (𝜑 → dom 𝐻 = ℝ) |
57 | 55, 56 | sseqtrrid 3954 |
. . . . . . 7
⊢ (𝜑 → (0[,)+∞) ⊆ dom
𝐻) |
58 | | funfvima2 7047 |
. . . . . . 7
⊢ ((Fun
𝐻 ∧ (0[,)+∞)
⊆ dom 𝐻) →
((𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)))) |
59 | 54, 57, 58 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ((𝑀‘(◡𝐹 “ {𝑥})) ∈ (0[,)+∞) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)))) |
60 | 15, 16, 59 | sylc 65 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞))) |
61 | | dmmeas 31881 |
. . . . . . . . . . . 12
⊢ (𝑀 ∈ ∪ ran measures → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
62 | 8, 61 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → dom 𝑀 ∈ ∪ ran
sigAlgebra) |
63 | 2 | fvexi 6731 |
. . . . . . . . . . . . . 14
⊢ 𝐽 ∈ V |
64 | 63 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ V) |
65 | 64 | sgsiga 31822 |
. . . . . . . . . . . 12
⊢ (𝜑 → (sigaGen‘𝐽) ∈ ∪ ran sigAlgebra) |
66 | 3, 65 | eqeltrid 2842 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑆 ∈ ∪ ran
sigAlgebra) |
67 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | sibfmbl 32014 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ (dom 𝑀MblFnM𝑆)) |
68 | 62, 66, 67 | mbfmf 31934 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:∪ dom 𝑀⟶∪ 𝑆) |
69 | 68 | frnd 6553 |
. . . . . . . . 9
⊢ (𝜑 → ran 𝐹 ⊆ ∪ 𝑆) |
70 | 3 | unieqi 4832 |
. . . . . . . . . . 11
⊢ ∪ 𝑆 =
∪ (sigaGen‘𝐽) |
71 | | unisg 31823 |
. . . . . . . . . . . 12
⊢ (𝐽 ∈ V → ∪ (sigaGen‘𝐽) = ∪ 𝐽) |
72 | 63, 71 | mp1i 13 |
. . . . . . . . . . 11
⊢ (𝜑 → ∪ (sigaGen‘𝐽) = ∪ 𝐽) |
73 | 70, 72 | syl5eq 2790 |
. . . . . . . . . 10
⊢ (𝜑 → ∪ 𝑆 =
∪ 𝐽) |
74 | | sitgclg.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑊 ∈ TopSp) |
75 | 1, 2 | tpsuni 21833 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ TopSp → 𝐵 = ∪
𝐽) |
76 | 74, 75 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 = ∪ 𝐽) |
77 | 73, 76 | eqtr4d 2780 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑆 =
𝐵) |
78 | 69, 77 | sseqtrd 3941 |
. . . . . . . 8
⊢ (𝜑 → ran 𝐹 ⊆ 𝐵) |
79 | 78 | ssdifd 4055 |
. . . . . . 7
⊢ (𝜑 → (ran 𝐹 ∖ { 0 }) ⊆ (𝐵 ∖ { 0 })) |
80 | 79 | sselda 3901 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝑥 ∈ (𝐵 ∖ { 0 })) |
81 | 80 | eldifad 3878 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → 𝑥 ∈ 𝐵) |
82 | | simp2 1139 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞))) |
83 | | eleq1 2825 |
. . . . . . . . 9
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (𝑚 ∈ (𝐻 “ (0[,)+∞)) ↔ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)))) |
84 | 83 | 3anbi2d 1443 |
. . . . . . . 8
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) ↔ (𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵))) |
85 | | oveq1 7220 |
. . . . . . . . 9
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (𝑚 · 𝑥) = ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) |
86 | 85 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → ((𝑚 · 𝑥) ∈ 𝐵 ↔ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)) |
87 | 84, 86 | imbi12d 348 |
. . . . . . 7
⊢ (𝑚 = (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) → (((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵) ↔ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵))) |
88 | | sitgclg.4 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → (𝑚 · 𝑥) ∈ 𝐵) |
89 | 87, 88 | vtoclg 3481 |
. . . . . 6
⊢ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) → ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵)) |
90 | 82, 89 | mpcom 38 |
. . . . 5
⊢ ((𝜑 ∧ (𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) ∈ (𝐻 “ (0[,)+∞)) ∧ 𝑥 ∈ 𝐵) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵) |
91 | 15, 60, 81, 90 | syl3anc 1373 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (ran 𝐹 ∖ { 0 })) → ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥) ∈ 𝐵) |
92 | 91 | fmpttd 6932 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)):(ran 𝐹 ∖ { 0 })⟶𝐵) |
93 | | mptexg 7037 |
. . . . . 6
⊢ ((ran
𝐹 ∖ { 0 }) ∈ V
→ (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ∈ V) |
94 | 14, 93 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ∈ V) |
95 | 4 | fvexi 6731 |
. . . . 5
⊢ 0 ∈
V |
96 | | suppimacnv 7916 |
. . . . 5
⊢ (((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ∈ V ∧ 0 ∈ V) → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) = (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 }))) |
97 | 94, 95, 96 | sylancl 589 |
. . . 4
⊢ (𝜑 → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) = (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 }))) |
98 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | sibfrn 32016 |
. . . . 5
⊢ (𝜑 → ran 𝐹 ∈ Fin) |
99 | | cnvimass 5949 |
. . . . . . 7
⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ dom (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) |
100 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) = (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) |
101 | 100 | dmmptss 6104 |
. . . . . . 7
⊢ dom
(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) ⊆ (ran 𝐹 ∖ { 0 }) |
102 | 99, 101 | sstri 3910 |
. . . . . 6
⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ (ran 𝐹 ∖ { 0 }) |
103 | | difss 4046 |
. . . . . 6
⊢ (ran
𝐹 ∖ { 0 }) ⊆
ran 𝐹 |
104 | 102, 103 | sstri 3910 |
. . . . 5
⊢ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ ran 𝐹 |
105 | | ssfi 8851 |
. . . . 5
⊢ ((ran
𝐹 ∈ Fin ∧ (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ⊆ ran 𝐹) → (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ∈
Fin) |
106 | 98, 104, 105 | sylancl 589 |
. . . 4
⊢ (𝜑 → (◡(𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) “ (V ∖ { 0 })) ∈
Fin) |
107 | 97, 106 | eqeltrd 2838 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥)) supp 0 ) ∈
Fin) |
108 | 1, 4, 11, 14, 92, 107 | gsumcl2 19299 |
. 2
⊢ (𝜑 → (𝑊 Σg (𝑥 ∈ (ran 𝐹 ∖ { 0 }) ↦ ((𝐻‘(𝑀‘(◡𝐹 “ {𝑥}))) · 𝑥))) ∈ 𝐵) |
109 | 10, 108 | eqeltrd 2838 |
1
⊢ (𝜑 → ((𝑊sitg𝑀)‘𝐹) ∈ 𝐵) |