# Metamath Proof Explorer

## Theorem smfco

Description: The composition of a Borel sigma-measurable function with a sigma-measurable function, is sigma-measurable. Proposition 121E (g) of Fremlin1 p. 37 . (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfco.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
smfco.f ${⊢}{\phi }\to {F}\in \mathrm{SMblFn}\left({S}\right)$
smfco.j ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
smfco.b ${⊢}{B}=\mathrm{SalGen}\left({J}\right)$
smfco.h ${⊢}{\phi }\to {H}\in \mathrm{SMblFn}\left({B}\right)$
Assertion smfco ${⊢}{\phi }\to {H}\circ {F}\in \mathrm{SMblFn}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 smfco.s ${⊢}{\phi }\to {S}\in \mathrm{SAlg}$
2 smfco.f ${⊢}{\phi }\to {F}\in \mathrm{SMblFn}\left({S}\right)$
3 smfco.j ${⊢}{J}=\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$
4 smfco.b ${⊢}{B}=\mathrm{SalGen}\left({J}\right)$
5 smfco.h ${⊢}{\phi }\to {H}\in \mathrm{SMblFn}\left({B}\right)$
6 nfv ${⊢}Ⅎ{a}\phantom{\rule{.4em}{0ex}}{\phi }$
7 cnvimass ${⊢}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\subseteq \mathrm{dom}{F}$
8 7 a1i ${⊢}{\phi }\to {{F}}^{-1}\left[\mathrm{dom}{H}\right]\subseteq \mathrm{dom}{F}$
9 eqid ${⊢}\mathrm{dom}{F}=\mathrm{dom}{F}$
10 1 2 9 smfdmss ${⊢}{\phi }\to \mathrm{dom}{F}\subseteq \bigcup {S}$
11 8 10 sstrd ${⊢}{\phi }\to {{F}}^{-1}\left[\mathrm{dom}{H}\right]\subseteq \bigcup {S}$
12 retop ${⊢}\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)\in \mathrm{Top}$
13 3 12 eqeltri ${⊢}{J}\in \mathrm{Top}$
14 13 a1i ${⊢}{\phi }\to {J}\in \mathrm{Top}$
15 14 4 salgencld ${⊢}{\phi }\to {B}\in \mathrm{SAlg}$
16 eqid ${⊢}\mathrm{dom}{H}=\mathrm{dom}{H}$
17 15 5 16 smff ${⊢}{\phi }\to {H}:\mathrm{dom}{H}⟶ℝ$
18 17 ffund ${⊢}{\phi }\to \mathrm{Fun}{H}$
19 1 2 9 smff ${⊢}{\phi }\to {F}:\mathrm{dom}{F}⟶ℝ$
20 19 ffund ${⊢}{\phi }\to \mathrm{Fun}{F}$
21 18 20 fco3 ${⊢}{\phi }\to \left({H}\circ {F}\right):{{F}}^{-1}\left[\mathrm{dom}{H}\right]⟶\mathrm{ran}{H}$
22 17 frnd ${⊢}{\phi }\to \mathrm{ran}{H}\subseteq ℝ$
23 21 22 fssd ${⊢}{\phi }\to \left({H}\circ {F}\right):{{F}}^{-1}\left[\mathrm{dom}{H}\right]⟶ℝ$
24 23 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left({H}\circ {F}\right):{{F}}^{-1}\left[\mathrm{dom}{H}\right]⟶ℝ$
25 rexr ${⊢}{a}\in ℝ\to {a}\in {ℝ}^{*}$
26 25 adantl ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {a}\in {ℝ}^{*}$
27 24 26 preimaioomnf ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {\left({H}\circ {F}\right)}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]=\left\{{x}\in {{F}}^{-1}\left[\mathrm{dom}{H}\right]|\left({H}\circ {F}\right)\left({x}\right)<{a}\right\}$
28 27 eqcomd ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left\{{x}\in {{F}}^{-1}\left[\mathrm{dom}{H}\right]|\left({H}\circ {F}\right)\left({x}\right)<{a}\right\}={\left({H}\circ {F}\right)}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]$
29 cnvco ${⊢}{\left({H}\circ {F}\right)}^{-1}={{F}}^{-1}\circ {{H}}^{-1}$
30 29 imaeq1i ${⊢}{\left({H}\circ {F}\right)}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]=\left({{F}}^{-1}\circ {{H}}^{-1}\right)\left[\left(\mathrm{-\infty },{a}\right)\right]$
31 30 a1i ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {\left({H}\circ {F}\right)}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]=\left({{F}}^{-1}\circ {{H}}^{-1}\right)\left[\left(\mathrm{-\infty },{a}\right)\right]$
32 imaco ${⊢}\left({{F}}^{-1}\circ {{H}}^{-1}\right)\left[\left(\mathrm{-\infty },{a}\right)\right]={{F}}^{-1}\left[{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\right]$
33 32 a1i ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left({{F}}^{-1}\circ {{H}}^{-1}\right)\left[\left(\mathrm{-\infty },{a}\right)\right]={{F}}^{-1}\left[{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\right]$
34 28 31 33 3eqtrd ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left\{{x}\in {{F}}^{-1}\left[\mathrm{dom}{H}\right]|\left({H}\circ {F}\right)\left({x}\right)<{a}\right\}={{F}}^{-1}\left[{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\right]$
35 17 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {H}:\mathrm{dom}{H}⟶ℝ$
36 35 26 preimaioomnf ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]=\left\{{x}\in \mathrm{dom}{H}|{H}\left({x}\right)<{a}\right\}$
37 36 eqcomd ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left\{{x}\in \mathrm{dom}{H}|{H}\left({x}\right)<{a}\right\}={{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]$
38 37 eqcomd ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]=\left\{{x}\in \mathrm{dom}{H}|{H}\left({x}\right)<{a}\right\}$
39 15 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {B}\in \mathrm{SAlg}$
40 5 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {H}\in \mathrm{SMblFn}\left({B}\right)$
41 simpr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {a}\in ℝ$
42 39 40 16 41 smfpreimalt ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left\{{x}\in \mathrm{dom}{H}|{H}\left({x}\right)<{a}\right\}\in \left({B}{↾}_{𝑡}\mathrm{dom}{H}\right)$
43 38 42 eqeltrd ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\in \left({B}{↾}_{𝑡}\mathrm{dom}{H}\right)$
44 15 elexd ${⊢}{\phi }\to {B}\in \mathrm{V}$
45 5 dmexd ${⊢}{\phi }\to \mathrm{dom}{H}\in \mathrm{V}$
46 elrest ${⊢}\left({B}\in \mathrm{V}\wedge \mathrm{dom}{H}\in \mathrm{V}\right)\to \left({{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\in \left({B}{↾}_{𝑡}\mathrm{dom}{H}\right)↔\exists {e}\in {B}\phantom{\rule{.4em}{0ex}}{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]={e}\cap \mathrm{dom}{H}\right)$
47 44 45 46 syl2anc ${⊢}{\phi }\to \left({{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\in \left({B}{↾}_{𝑡}\mathrm{dom}{H}\right)↔\exists {e}\in {B}\phantom{\rule{.4em}{0ex}}{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]={e}\cap \mathrm{dom}{H}\right)$
48 47 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left({{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\in \left({B}{↾}_{𝑡}\mathrm{dom}{H}\right)↔\exists {e}\in {B}\phantom{\rule{.4em}{0ex}}{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]={e}\cap \mathrm{dom}{H}\right)$
49 43 48 mpbid ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \exists {e}\in {B}\phantom{\rule{.4em}{0ex}}{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]={e}\cap \mathrm{dom}{H}$
50 imaeq2 ${⊢}{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]={e}\cap \mathrm{dom}{H}\to {{F}}^{-1}\left[{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\right]={{F}}^{-1}\left[{e}\cap \mathrm{dom}{H}\right]$
51 50 3ad2ant3 ${⊢}\left({\phi }\wedge {e}\in {B}\wedge {{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]={e}\cap \mathrm{dom}{H}\right)\to {{F}}^{-1}\left[{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\right]={{F}}^{-1}\left[{e}\cap \mathrm{dom}{H}\right]$
52 ovexd ${⊢}\left({\phi }\wedge {e}\in {B}\right)\to {S}{↾}_{𝑡}\mathrm{dom}{F}\in \mathrm{V}$
53 2 elexd ${⊢}{\phi }\to {F}\in \mathrm{V}$
54 cnvexg ${⊢}{F}\in \mathrm{V}\to {{F}}^{-1}\in \mathrm{V}$
55 53 54 syl ${⊢}{\phi }\to {{F}}^{-1}\in \mathrm{V}$
56 imaexg ${⊢}{{F}}^{-1}\in \mathrm{V}\to {{F}}^{-1}\left[\mathrm{dom}{H}\right]\in \mathrm{V}$
57 55 56 syl ${⊢}{\phi }\to {{F}}^{-1}\left[\mathrm{dom}{H}\right]\in \mathrm{V}$
58 57 adantr ${⊢}\left({\phi }\wedge {e}\in {B}\right)\to {{F}}^{-1}\left[\mathrm{dom}{H}\right]\in \mathrm{V}$
59 1 adantr ${⊢}\left({\phi }\wedge {e}\in {B}\right)\to {S}\in \mathrm{SAlg}$
60 2 adantr ${⊢}\left({\phi }\wedge {e}\in {B}\right)\to {F}\in \mathrm{SMblFn}\left({S}\right)$
61 simpr ${⊢}\left({\phi }\wedge {e}\in {B}\right)\to {e}\in {B}$
62 eqid ${⊢}{{F}}^{-1}\left[{e}\right]={{F}}^{-1}\left[{e}\right]$
63 59 60 9 3 4 61 62 smfpimbor1 ${⊢}\left({\phi }\wedge {e}\in {B}\right)\to {{F}}^{-1}\left[{e}\right]\in \left({S}{↾}_{𝑡}\mathrm{dom}{F}\right)$
64 eqid ${⊢}{{F}}^{-1}\left[{e}\right]\cap {{F}}^{-1}\left[\mathrm{dom}{H}\right]={{F}}^{-1}\left[{e}\right]\cap {{F}}^{-1}\left[\mathrm{dom}{H}\right]$
65 52 58 63 64 elrestd ${⊢}\left({\phi }\wedge {e}\in {B}\right)\to {{F}}^{-1}\left[{e}\right]\cap {{F}}^{-1}\left[\mathrm{dom}{H}\right]\in \left(\left({S}{↾}_{𝑡}\mathrm{dom}{F}\right){↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\right)$
66 inpreima ${⊢}\mathrm{Fun}{F}\to {{F}}^{-1}\left[{e}\cap \mathrm{dom}{H}\right]={{F}}^{-1}\left[{e}\right]\cap {{F}}^{-1}\left[\mathrm{dom}{H}\right]$
67 20 66 syl ${⊢}{\phi }\to {{F}}^{-1}\left[{e}\cap \mathrm{dom}{H}\right]={{F}}^{-1}\left[{e}\right]\cap {{F}}^{-1}\left[\mathrm{dom}{H}\right]$
68 67 adantr ${⊢}\left({\phi }\wedge {e}\in {B}\right)\to {{F}}^{-1}\left[{e}\cap \mathrm{dom}{H}\right]={{F}}^{-1}\left[{e}\right]\cap {{F}}^{-1}\left[\mathrm{dom}{H}\right]$
69 2 dmexd ${⊢}{\phi }\to \mathrm{dom}{F}\in \mathrm{V}$
70 restabs ${⊢}\left({S}\in \mathrm{SAlg}\wedge {{F}}^{-1}\left[\mathrm{dom}{H}\right]\subseteq \mathrm{dom}{F}\wedge \mathrm{dom}{F}\in \mathrm{V}\right)\to \left({S}{↾}_{𝑡}\mathrm{dom}{F}\right){↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]={S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]$
71 1 8 69 70 syl3anc ${⊢}{\phi }\to \left({S}{↾}_{𝑡}\mathrm{dom}{F}\right){↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]={S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]$
72 71 eqcomd ${⊢}{\phi }\to {S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]=\left({S}{↾}_{𝑡}\mathrm{dom}{F}\right){↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]$
73 72 adantr ${⊢}\left({\phi }\wedge {e}\in {B}\right)\to {S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]=\left({S}{↾}_{𝑡}\mathrm{dom}{F}\right){↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]$
74 68 73 eleq12d ${⊢}\left({\phi }\wedge {e}\in {B}\right)\to \left({{F}}^{-1}\left[{e}\cap \mathrm{dom}{H}\right]\in \left({S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\right)↔{{F}}^{-1}\left[{e}\right]\cap {{F}}^{-1}\left[\mathrm{dom}{H}\right]\in \left(\left({S}{↾}_{𝑡}\mathrm{dom}{F}\right){↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\right)\right)$
75 65 74 mpbird ${⊢}\left({\phi }\wedge {e}\in {B}\right)\to {{F}}^{-1}\left[{e}\cap \mathrm{dom}{H}\right]\in \left({S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\right)$
76 75 3adant3 ${⊢}\left({\phi }\wedge {e}\in {B}\wedge {{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]={e}\cap \mathrm{dom}{H}\right)\to {{F}}^{-1}\left[{e}\cap \mathrm{dom}{H}\right]\in \left({S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\right)$
77 51 76 eqeltrd ${⊢}\left({\phi }\wedge {e}\in {B}\wedge {{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]={e}\cap \mathrm{dom}{H}\right)\to {{F}}^{-1}\left[{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\right]\in \left({S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\right)$
78 77 3exp ${⊢}{\phi }\to \left({e}\in {B}\to \left({{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]={e}\cap \mathrm{dom}{H}\to {{F}}^{-1}\left[{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\right]\in \left({S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\right)\right)\right)$
79 78 adantr ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left({e}\in {B}\to \left({{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]={e}\cap \mathrm{dom}{H}\to {{F}}^{-1}\left[{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\right]\in \left({S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\right)\right)\right)$
80 79 rexlimdv ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left(\exists {e}\in {B}\phantom{\rule{.4em}{0ex}}{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]={e}\cap \mathrm{dom}{H}\to {{F}}^{-1}\left[{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\right]\in \left({S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\right)\right)$
81 49 80 mpd ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to {{F}}^{-1}\left[{{H}}^{-1}\left[\left(\mathrm{-\infty },{a}\right)\right]\right]\in \left({S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\right)$
82 34 81 eqeltrd ${⊢}\left({\phi }\wedge {a}\in ℝ\right)\to \left\{{x}\in {{F}}^{-1}\left[\mathrm{dom}{H}\right]|\left({H}\circ {F}\right)\left({x}\right)<{a}\right\}\in \left({S}{↾}_{𝑡}{{F}}^{-1}\left[\mathrm{dom}{H}\right]\right)$
83 6 1 11 23 82 issmfd ${⊢}{\phi }\to {H}\circ {F}\in \mathrm{SMblFn}\left({S}\right)$