Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smfco Structured version   Visualization version   GIF version

Theorem smfco 41804
 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.)
Hypotheses
Ref Expression
smfco.s (𝜑𝑆 ∈ SAlg)
smfco.f (𝜑𝐹 ∈ (SMblFn‘𝑆))
smfco.j 𝐽 = (topGen‘ran (,))
smfco.b 𝐵 = (SalGen‘𝐽)
smfco.h (𝜑𝐻 ∈ (SMblFn‘𝐵))
Assertion
Ref Expression
smfco (𝜑 → (𝐻𝐹) ∈ (SMblFn‘𝑆))

Proof of Theorem smfco
Dummy variables 𝑒 𝑎 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 2015 . 2 𝑎𝜑
2 smfco.s . 2 (𝜑𝑆 ∈ SAlg)
3 cnvimass 5727 . . . 4 (𝐹 “ dom 𝐻) ⊆ dom 𝐹
43a1i 11 . . 3 (𝜑 → (𝐹 “ dom 𝐻) ⊆ dom 𝐹)
5 smfco.f . . . 4 (𝜑𝐹 ∈ (SMblFn‘𝑆))
6 eqid 2826 . . . 4 dom 𝐹 = dom 𝐹
72, 5, 6smfdmss 41737 . . 3 (𝜑 → dom 𝐹 𝑆)
84, 7sstrd 3838 . 2 (𝜑 → (𝐹 “ dom 𝐻) ⊆ 𝑆)
9 smfco.j . . . . . . . . 9 𝐽 = (topGen‘ran (,))
10 retop 22936 . . . . . . . . 9 (topGen‘ran (,)) ∈ Top
119, 10eqeltri 2903 . . . . . . . 8 𝐽 ∈ Top
1211a1i 11 . . . . . . 7 (𝜑𝐽 ∈ Top)
13 smfco.b . . . . . . 7 𝐵 = (SalGen‘𝐽)
1412, 13salgencld 41359 . . . . . 6 (𝜑𝐵 ∈ SAlg)
15 smfco.h . . . . . 6 (𝜑𝐻 ∈ (SMblFn‘𝐵))
16 eqid 2826 . . . . . 6 dom 𝐻 = dom 𝐻
1714, 15, 16smff 41736 . . . . 5 (𝜑𝐻:dom 𝐻⟶ℝ)
1817ffund 6283 . . . 4 (𝜑 → Fun 𝐻)
192, 5, 6smff 41736 . . . . 5 (𝜑𝐹:dom 𝐹⟶ℝ)
2019ffund 6283 . . . 4 (𝜑 → Fun 𝐹)
2118, 20fco3 40227 . . 3 (𝜑 → (𝐻𝐹):(𝐹 “ dom 𝐻)⟶ran 𝐻)
2217frnd 6286 . . 3 (𝜑 → ran 𝐻 ⊆ ℝ)
2321, 22fssd 6293 . 2 (𝜑 → (𝐻𝐹):(𝐹 “ dom 𝐻)⟶ℝ)
2423adantr 474 . . . . . 6 ((𝜑𝑎 ∈ ℝ) → (𝐻𝐹):(𝐹 “ dom 𝐻)⟶ℝ)
25 rexr 10403 . . . . . . 7 (𝑎 ∈ ℝ → 𝑎 ∈ ℝ*)
2625adantl 475 . . . . . 6 ((𝜑𝑎 ∈ ℝ) → 𝑎 ∈ ℝ*)
2724, 26preimaioomnf 41724 . . . . 5 ((𝜑𝑎 ∈ ℝ) → ((𝐻𝐹) “ (-∞(,)𝑎)) = {𝑥 ∈ (𝐹 “ dom 𝐻) ∣ ((𝐻𝐹)‘𝑥) < 𝑎})
2827eqcomd 2832 . . . 4 ((𝜑𝑎 ∈ ℝ) → {𝑥 ∈ (𝐹 “ dom 𝐻) ∣ ((𝐻𝐹)‘𝑥) < 𝑎} = ((𝐻𝐹) “ (-∞(,)𝑎)))
29 cnvco 5541 . . . . . 6 (𝐻𝐹) = (𝐹𝐻)
3029imaeq1i 5705 . . . . 5 ((𝐻𝐹) “ (-∞(,)𝑎)) = ((𝐹𝐻) “ (-∞(,)𝑎))
3130a1i 11 . . . 4 ((𝜑𝑎 ∈ ℝ) → ((𝐻𝐹) “ (-∞(,)𝑎)) = ((𝐹𝐻) “ (-∞(,)𝑎)))
32 imaco 5882 . . . . 5 ((𝐹𝐻) “ (-∞(,)𝑎)) = (𝐹 “ (𝐻 “ (-∞(,)𝑎)))
3332a1i 11 . . . 4 ((𝜑𝑎 ∈ ℝ) → ((𝐹𝐻) “ (-∞(,)𝑎)) = (𝐹 “ (𝐻 “ (-∞(,)𝑎))))
3428, 31, 333eqtrd 2866 . . 3 ((𝜑𝑎 ∈ ℝ) → {𝑥 ∈ (𝐹 “ dom 𝐻) ∣ ((𝐻𝐹)‘𝑥) < 𝑎} = (𝐹 “ (𝐻 “ (-∞(,)𝑎))))
3517adantr 474 . . . . . . . . 9 ((𝜑𝑎 ∈ ℝ) → 𝐻:dom 𝐻⟶ℝ)
3635, 26preimaioomnf 41724 . . . . . . . 8 ((𝜑𝑎 ∈ ℝ) → (𝐻 “ (-∞(,)𝑎)) = {𝑥 ∈ dom 𝐻 ∣ (𝐻𝑥) < 𝑎})
3736eqcomd 2832 . . . . . . 7 ((𝜑𝑎 ∈ ℝ) → {𝑥 ∈ dom 𝐻 ∣ (𝐻𝑥) < 𝑎} = (𝐻 “ (-∞(,)𝑎)))
3837eqcomd 2832 . . . . . 6 ((𝜑𝑎 ∈ ℝ) → (𝐻 “ (-∞(,)𝑎)) = {𝑥 ∈ dom 𝐻 ∣ (𝐻𝑥) < 𝑎})
3914adantr 474 . . . . . . 7 ((𝜑𝑎 ∈ ℝ) → 𝐵 ∈ SAlg)
4015adantr 474 . . . . . . 7 ((𝜑𝑎 ∈ ℝ) → 𝐻 ∈ (SMblFn‘𝐵))
41 simpr 479 . . . . . . 7 ((𝜑𝑎 ∈ ℝ) → 𝑎 ∈ ℝ)
4239, 40, 16, 41smfpreimalt 41735 . . . . . 6 ((𝜑𝑎 ∈ ℝ) → {𝑥 ∈ dom 𝐻 ∣ (𝐻𝑥) < 𝑎} ∈ (𝐵t dom 𝐻))
4338, 42eqeltrd 2907 . . . . 5 ((𝜑𝑎 ∈ ℝ) → (𝐻 “ (-∞(,)𝑎)) ∈ (𝐵t dom 𝐻))
4414elexd 3432 . . . . . . 7 (𝜑𝐵 ∈ V)
4515dmexd 7361 . . . . . . 7 (𝜑 → dom 𝐻 ∈ V)
46 elrest 16442 . . . . . . 7 ((𝐵 ∈ V ∧ dom 𝐻 ∈ V) → ((𝐻 “ (-∞(,)𝑎)) ∈ (𝐵t dom 𝐻) ↔ ∃𝑒𝐵 (𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)))
4744, 45, 46syl2anc 581 . . . . . 6 (𝜑 → ((𝐻 “ (-∞(,)𝑎)) ∈ (𝐵t dom 𝐻) ↔ ∃𝑒𝐵 (𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)))
4847adantr 474 . . . . 5 ((𝜑𝑎 ∈ ℝ) → ((𝐻 “ (-∞(,)𝑎)) ∈ (𝐵t dom 𝐻) ↔ ∃𝑒𝐵 (𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)))
4943, 48mpbid 224 . . . 4 ((𝜑𝑎 ∈ ℝ) → ∃𝑒𝐵 (𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻))
50 imaeq2 5704 . . . . . . . . 9 ((𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (𝐹 “ (𝐻 “ (-∞(,)𝑎))) = (𝐹 “ (𝑒 ∩ dom 𝐻)))
51503ad2ant3 1171 . . . . . . . 8 ((𝜑𝑒𝐵 ∧ (𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)) → (𝐹 “ (𝐻 “ (-∞(,)𝑎))) = (𝐹 “ (𝑒 ∩ dom 𝐻)))
52 ovexd 6940 . . . . . . . . . . 11 ((𝜑𝑒𝐵) → (𝑆t dom 𝐹) ∈ V)
535elexd 3432 . . . . . . . . . . . . . 14 (𝜑𝐹 ∈ V)
54 cnvexg 7375 . . . . . . . . . . . . . 14 (𝐹 ∈ V → 𝐹 ∈ V)
5553, 54syl 17 . . . . . . . . . . . . 13 (𝜑𝐹 ∈ V)
56 imaexg 7366 . . . . . . . . . . . . 13 (𝐹 ∈ V → (𝐹 “ dom 𝐻) ∈ V)
5755, 56syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹 “ dom 𝐻) ∈ V)
5857adantr 474 . . . . . . . . . . 11 ((𝜑𝑒𝐵) → (𝐹 “ dom 𝐻) ∈ V)
592adantr 474 . . . . . . . . . . . 12 ((𝜑𝑒𝐵) → 𝑆 ∈ SAlg)
605adantr 474 . . . . . . . . . . . 12 ((𝜑𝑒𝐵) → 𝐹 ∈ (SMblFn‘𝑆))
61 simpr 479 . . . . . . . . . . . 12 ((𝜑𝑒𝐵) → 𝑒𝐵)
62 eqid 2826 . . . . . . . . . . . 12 (𝐹𝑒) = (𝐹𝑒)
6359, 60, 6, 9, 13, 61, 62smfpimbor1 41802 . . . . . . . . . . 11 ((𝜑𝑒𝐵) → (𝐹𝑒) ∈ (𝑆t dom 𝐹))
64 eqid 2826 . . . . . . . . . . 11 ((𝐹𝑒) ∩ (𝐹 “ dom 𝐻)) = ((𝐹𝑒) ∩ (𝐹 “ dom 𝐻))
6552, 58, 63, 64elrestd 40107 . . . . . . . . . 10 ((𝜑𝑒𝐵) → ((𝐹𝑒) ∩ (𝐹 “ dom 𝐻)) ∈ ((𝑆t dom 𝐹) ↾t (𝐹 “ dom 𝐻)))
66 inpreima 6592 . . . . . . . . . . . . 13 (Fun 𝐹 → (𝐹 “ (𝑒 ∩ dom 𝐻)) = ((𝐹𝑒) ∩ (𝐹 “ dom 𝐻)))
6720, 66syl 17 . . . . . . . . . . . 12 (𝜑 → (𝐹 “ (𝑒 ∩ dom 𝐻)) = ((𝐹𝑒) ∩ (𝐹 “ dom 𝐻)))
6867adantr 474 . . . . . . . . . . 11 ((𝜑𝑒𝐵) → (𝐹 “ (𝑒 ∩ dom 𝐻)) = ((𝐹𝑒) ∩ (𝐹 “ dom 𝐻)))
695dmexd 7361 . . . . . . . . . . . . . 14 (𝜑 → dom 𝐹 ∈ V)
70 restabs 21341 . . . . . . . . . . . . . 14 ((𝑆 ∈ SAlg ∧ (𝐹 “ dom 𝐻) ⊆ dom 𝐹 ∧ dom 𝐹 ∈ V) → ((𝑆t dom 𝐹) ↾t (𝐹 “ dom 𝐻)) = (𝑆t (𝐹 “ dom 𝐻)))
712, 4, 69, 70syl3anc 1496 . . . . . . . . . . . . 13 (𝜑 → ((𝑆t dom 𝐹) ↾t (𝐹 “ dom 𝐻)) = (𝑆t (𝐹 “ dom 𝐻)))
7271eqcomd 2832 . . . . . . . . . . . 12 (𝜑 → (𝑆t (𝐹 “ dom 𝐻)) = ((𝑆t dom 𝐹) ↾t (𝐹 “ dom 𝐻)))
7372adantr 474 . . . . . . . . . . 11 ((𝜑𝑒𝐵) → (𝑆t (𝐹 “ dom 𝐻)) = ((𝑆t dom 𝐹) ↾t (𝐹 “ dom 𝐻)))
7468, 73eleq12d 2901 . . . . . . . . . 10 ((𝜑𝑒𝐵) → ((𝐹 “ (𝑒 ∩ dom 𝐻)) ∈ (𝑆t (𝐹 “ dom 𝐻)) ↔ ((𝐹𝑒) ∩ (𝐹 “ dom 𝐻)) ∈ ((𝑆t dom 𝐹) ↾t (𝐹 “ dom 𝐻))))
7565, 74mpbird 249 . . . . . . . . 9 ((𝜑𝑒𝐵) → (𝐹 “ (𝑒 ∩ dom 𝐻)) ∈ (𝑆t (𝐹 “ dom 𝐻)))
76753adant3 1168 . . . . . . . 8 ((𝜑𝑒𝐵 ∧ (𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)) → (𝐹 “ (𝑒 ∩ dom 𝐻)) ∈ (𝑆t (𝐹 “ dom 𝐻)))
7751, 76eqeltrd 2907 . . . . . . 7 ((𝜑𝑒𝐵 ∧ (𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻)) → (𝐹 “ (𝐻 “ (-∞(,)𝑎))) ∈ (𝑆t (𝐹 “ dom 𝐻)))
78773exp 1154 . . . . . 6 (𝜑 → (𝑒𝐵 → ((𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (𝐹 “ (𝐻 “ (-∞(,)𝑎))) ∈ (𝑆t (𝐹 “ dom 𝐻)))))
7978adantr 474 . . . . 5 ((𝜑𝑎 ∈ ℝ) → (𝑒𝐵 → ((𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (𝐹 “ (𝐻 “ (-∞(,)𝑎))) ∈ (𝑆t (𝐹 “ dom 𝐻)))))
8079rexlimdv 3240 . . . 4 ((𝜑𝑎 ∈ ℝ) → (∃𝑒𝐵 (𝐻 “ (-∞(,)𝑎)) = (𝑒 ∩ dom 𝐻) → (𝐹 “ (𝐻 “ (-∞(,)𝑎))) ∈ (𝑆t (𝐹 “ dom 𝐻))))
8149, 80mpd 15 . . 3 ((𝜑𝑎 ∈ ℝ) → (𝐹 “ (𝐻 “ (-∞(,)𝑎))) ∈ (𝑆t (𝐹 “ dom 𝐻)))
8234, 81eqeltrd 2907 . 2 ((𝜑𝑎 ∈ ℝ) → {𝑥 ∈ (𝐹 “ dom 𝐻) ∣ ((𝐻𝐹)‘𝑥) < 𝑎} ∈ (𝑆t (𝐹 “ dom 𝐻)))
831, 2, 8, 23, 82issmfd 41739 1 (𝜑 → (𝐻𝐹) ∈ (SMblFn‘𝑆))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 386   ∧ w3a 1113   = wceq 1658   ∈ wcel 2166  ∃wrex 3119  {crab 3122  Vcvv 3415   ∩ cin 3798   ⊆ wss 3799  ∪ cuni 4659   class class class wbr 4874  ◡ccnv 5342  dom cdm 5343  ran crn 5344   “ cima 5346   ∘ ccom 5347  Fun wfun 6118  ⟶wf 6120  ‘cfv 6124  (class class class)co 6906  ℝcr 10252  -∞cmnf 10390  ℝ*cxr 10391   < clt 10392  (,)cioo 12464   ↾t crest 16435  topGenctg 16452  Topctop 21069  SAlgcsalg 41320  SalGencsalgen 41324  SMblFncsmblfn 41704 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-8 2168  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2804  ax-rep 4995  ax-sep 5006  ax-nul 5014  ax-pow 5066  ax-pr 5128  ax-un 7210  ax-inf2 8816  ax-cc 9573  ax-ac2 9601  ax-cnex 10309  ax-resscn 10310  ax-1cn 10311  ax-icn 10312  ax-addcl 10313  ax-addrcl 10314  ax-mulcl 10315  ax-mulrcl 10316  ax-mulcom 10317  ax-addass 10318  ax-mulass 10319  ax-distr 10320  ax-i2m1 10321  ax-1ne0 10322  ax-1rid 10323  ax-rnegex 10324  ax-rrecex 10325  ax-cnre 10326  ax-pre-lttri 10327  ax-pre-lttrn 10328  ax-pre-ltadd 10329  ax-pre-mulgt0 10330  ax-pre-sup 10331 This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3or 1114  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2606  df-eu 2641  df-clab 2813  df-cleq 2819  df-clel 2822  df-nfc 2959  df-ne 3001  df-nel 3104  df-ral 3123  df-rex 3124  df-reu 3125  df-rmo 3126  df-rab 3127  df-v 3417  df-sbc 3664  df-csb 3759  df-dif 3802  df-un 3804  df-in 3806  df-ss 3813  df-pss 3815  df-nul 4146  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4660  df-int 4699  df-iun 4743  df-iin 4744  df-br 4875  df-opab 4937  df-mpt 4954  df-tr 4977  df-id 5251  df-eprel 5256  df-po 5264  df-so 5265  df-fr 5302  df-se 5303  df-we 5304  df-xp 5349  df-rel 5350  df-cnv 5351  df-co 5352  df-dm 5353  df-rn 5354  df-res 5355  df-ima 5356  df-pred 5921  df-ord 5967  df-on 5968  df-lim 5969  df-suc 5970  df-iota 6087  df-fun 6126  df-fn 6127  df-f 6128  df-f1 6129  df-fo 6130  df-f1o 6131  df-fv 6132  df-isom 6133  df-riota 6867  df-ov 6909  df-oprab 6910  df-mpt2 6911  df-om 7328  df-1st 7429  df-2nd 7430  df-wrecs 7673  df-recs 7735  df-rdg 7773  df-1o 7827  df-oadd 7831  df-omul 7832  df-er 8010  df-map 8125  df-pm 8126  df-en 8224  df-dom 8225  df-sdom 8226  df-fin 8227  df-sup 8618  df-inf 8619  df-oi 8685  df-card 9079  df-acn 9082  df-ac 9253  df-pnf 10394  df-mnf 10395  df-xr 10396  df-ltxr 10397  df-le 10398  df-sub 10588  df-neg 10589  df-div 11011  df-nn 11352  df-n0 11620  df-z 11706  df-uz 11970  df-q 12073  df-rp 12114  df-ioo 12468  df-ico 12470  df-fl 12889  df-rest 16437  df-topgen 16458  df-top 21070  df-bases 21122  df-salg 41321  df-salgen 41325  df-smblfn 41705 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator