Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  smfco Structured version   Visualization version   GIF version
Theorem smfco 45196
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 1917 . 2 β„²π‘Žπœ‘
2 smfco.s . 2 (πœ‘ β†’ 𝑆 ∈ SAlg)
3 cnvimass 6053 . . . 4 (◑𝐹 β€œ dom 𝐻) βŠ† dom 𝐹
43a1i 11 . . 3 (πœ‘ β†’ (◑𝐹 β€œ dom 𝐻) βŠ† dom 𝐹)
5 smfco.f . . . 4 (πœ‘ β†’ 𝐹 ∈ (SMblFnβ€˜π‘†))
6 eqid 2731 . . . 4 dom 𝐹 = dom 𝐹
72, 5, 6smfdmss 45127 . . 3 (πœ‘ β†’ dom 𝐹 βŠ† βˆͺ 𝑆)
84, 7sstrd 3972 . 2 (πœ‘ β†’ (◑𝐹 β€œ dom 𝐻) βŠ† βˆͺ 𝑆)
9 smfco.j . . . . . . . . 9 𝐽 = (topGenβ€˜ran (,))
10 retop 24177 . . . . . . . . 9 (topGenβ€˜ran (,)) ∈ Top
119, 10eqeltri 2828 . . . . . . . 8 𝐽 ∈ Top
1211a1i 11 . . . . . . 7 (πœ‘ β†’ 𝐽 ∈ Top)
13 smfco.b . . . . . . 7 𝐡 = (SalGenβ€˜π½)
1412, 13salgencld 44743 . . . . . 6 (πœ‘ β†’ 𝐡 ∈ SAlg)
15 smfco.h . . . . . 6 (πœ‘ β†’ 𝐻 ∈ (SMblFnβ€˜π΅))
16 eqid 2731 . . . . . 6 dom 𝐻 = dom 𝐻
1714, 15, 16smff 45126 . . . . 5 (πœ‘ β†’ 𝐻:dom π»βŸΆβ„)
1817ffund 6692 . . . 4 (πœ‘ β†’ Fun 𝐻)
192, 5, 6smff 45126 . . . . 5 (πœ‘ β†’ 𝐹:dom πΉβŸΆβ„)
2019ffund 6692 . . . 4 (πœ‘ β†’ Fun 𝐹)
2118, 20funcofd 6721 . . 3 (πœ‘ β†’ (𝐻 ∘ 𝐹):(◑𝐹 β€œ dom 𝐻)⟢ran 𝐻)
2217frnd 6696 . . 3 (πœ‘ β†’ ran 𝐻 βŠ† ℝ)
2321, 22fssd 6706 . 2 (πœ‘ β†’ (𝐻 ∘ 𝐹):(◑𝐹 β€œ dom 𝐻)βŸΆβ„)
24 cnvco 5861 . . . . 5 β—‘(𝐻 ∘ 𝐹) = (◑𝐹 ∘ ◑𝐻)
2524imaeq1i 6030 . . . 4 (β—‘(𝐻 ∘ 𝐹) β€œ (-∞(,)π‘Ž)) = ((◑𝐹 ∘ ◑𝐻) β€œ (-∞(,)π‘Ž))
2623adantr 481 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (𝐻 ∘ 𝐹):(◑𝐹 β€œ dom 𝐻)βŸΆβ„)
27 rexr 11225 . . . . . 6 (π‘Ž ∈ ℝ β†’ π‘Ž ∈ ℝ*)
2827adantl 482 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ π‘Ž ∈ ℝ*)
2926, 28preimaioomnf 45113 . . . 4 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (β—‘(𝐻 ∘ 𝐹) β€œ (-∞(,)π‘Ž)) = {π‘₯ ∈ (◑𝐹 β€œ dom 𝐻) ∣ ((𝐻 ∘ 𝐹)β€˜π‘₯) < π‘Ž})
30 imaco 6223 . . . . 5 ((◑𝐹 ∘ ◑𝐻) β€œ (-∞(,)π‘Ž)) = (◑𝐹 β€œ (◑𝐻 β€œ (-∞(,)π‘Ž)))
3130a1i 11 . . . 4 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ ((◑𝐹 ∘ ◑𝐻) β€œ (-∞(,)π‘Ž)) = (◑𝐹 β€œ (◑𝐻 β€œ (-∞(,)π‘Ž))))
3225, 29, 313eqtr3a 2795 . . 3 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ {π‘₯ ∈ (◑𝐹 β€œ dom 𝐻) ∣ ((𝐻 ∘ 𝐹)β€˜π‘₯) < π‘Ž} = (◑𝐹 β€œ (◑𝐻 β€œ (-∞(,)π‘Ž))))
3317adantr 481 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ 𝐻:dom π»βŸΆβ„)
3433, 28preimaioomnf 45113 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (◑𝐻 β€œ (-∞(,)π‘Ž)) = {π‘₯ ∈ dom 𝐻 ∣ (π»β€˜π‘₯) < π‘Ž})
3514adantr 481 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ 𝐡 ∈ SAlg)
3615adantr 481 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ 𝐻 ∈ (SMblFnβ€˜π΅))
37 simpr 485 . . . . . . 7 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ π‘Ž ∈ ℝ)
3835, 36, 16, 37smfpreimalt 45125 . . . . . 6 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ {π‘₯ ∈ dom 𝐻 ∣ (π»β€˜π‘₯) < π‘Ž} ∈ (𝐡 β†Ύt dom 𝐻))
3934, 38eqeltrd 2832 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (◑𝐻 β€œ (-∞(,)π‘Ž)) ∈ (𝐡 β†Ύt dom 𝐻))
4014elexd 3479 . . . . . . 7 (πœ‘ β†’ 𝐡 ∈ V)
4115dmexd 7862 . . . . . . 7 (πœ‘ β†’ dom 𝐻 ∈ V)
42 elrest 17338 . . . . . . 7 ((𝐡 ∈ V ∧ dom 𝐻 ∈ V) β†’ ((◑𝐻 β€œ (-∞(,)π‘Ž)) ∈ (𝐡 β†Ύt dom 𝐻) ↔ βˆƒπ‘’ ∈ 𝐡 (◑𝐻 β€œ (-∞(,)π‘Ž)) = (𝑒 ∩ dom 𝐻)))
4340, 41, 42syl2anc 584 . . . . . 6 (πœ‘ β†’ ((◑𝐻 β€œ (-∞(,)π‘Ž)) ∈ (𝐡 β†Ύt dom 𝐻) ↔ βˆƒπ‘’ ∈ 𝐡 (◑𝐻 β€œ (-∞(,)π‘Ž)) = (𝑒 ∩ dom 𝐻)))
4443adantr 481 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ ((◑𝐻 β€œ (-∞(,)π‘Ž)) ∈ (𝐡 β†Ύt dom 𝐻) ↔ βˆƒπ‘’ ∈ 𝐡 (◑𝐻 β€œ (-∞(,)π‘Ž)) = (𝑒 ∩ dom 𝐻)))
4539, 44mpbid 231 . . . 4 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ βˆƒπ‘’ ∈ 𝐡 (◑𝐻 β€œ (-∞(,)π‘Ž)) = (𝑒 ∩ dom 𝐻))
46 imaeq2 6029 . . . . . . . . 9 ((◑𝐻 β€œ (-∞(,)π‘Ž)) = (𝑒 ∩ dom 𝐻) β†’ (◑𝐹 β€œ (◑𝐻 β€œ (-∞(,)π‘Ž))) = (◑𝐹 β€œ (𝑒 ∩ dom 𝐻)))
47463ad2ant3 1135 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ 𝐡 ∧ (◑𝐻 β€œ (-∞(,)π‘Ž)) = (𝑒 ∩ dom 𝐻)) β†’ (◑𝐹 β€œ (◑𝐻 β€œ (-∞(,)π‘Ž))) = (◑𝐹 β€œ (𝑒 ∩ dom 𝐻)))
48 ovexd 7412 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ 𝐡) β†’ (𝑆 β†Ύt dom 𝐹) ∈ V)
495elexd 3479 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐹 ∈ V)
50 cnvexg 7881 . . . . . . . . . . . . 13 (𝐹 ∈ V β†’ ◑𝐹 ∈ V)
51 imaexg 7872 . . . . . . . . . . . . 13 (◑𝐹 ∈ V β†’ (◑𝐹 β€œ dom 𝐻) ∈ V)
5249, 50, 513syl 18 . . . . . . . . . . . 12 (πœ‘ β†’ (◑𝐹 β€œ dom 𝐻) ∈ V)
5352adantr 481 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ 𝐡) β†’ (◑𝐹 β€œ dom 𝐻) ∈ V)
542adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ 𝐡) β†’ 𝑆 ∈ SAlg)
555adantr 481 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ 𝐡) β†’ 𝐹 ∈ (SMblFnβ€˜π‘†))
56 simpr 485 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝑒 ∈ 𝐡) β†’ 𝑒 ∈ 𝐡)
57 eqid 2731 . . . . . . . . . . . 12 (◑𝐹 β€œ 𝑒) = (◑𝐹 β€œ 𝑒)
5854, 55, 6, 9, 13, 56, 57smfpimbor1 45194 . . . . . . . . . . 11 ((πœ‘ ∧ 𝑒 ∈ 𝐡) β†’ (◑𝐹 β€œ 𝑒) ∈ (𝑆 β†Ύt dom 𝐹))
59 eqid 2731 . . . . . . . . . . 11 ((◑𝐹 β€œ 𝑒) ∩ (◑𝐹 β€œ dom 𝐻)) = ((◑𝐹 β€œ 𝑒) ∩ (◑𝐹 β€œ dom 𝐻))
6048, 53, 58, 59elrestd 43473 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ 𝐡) β†’ ((◑𝐹 β€œ 𝑒) ∩ (◑𝐹 β€œ dom 𝐻)) ∈ ((𝑆 β†Ύt dom 𝐹) β†Ύt (◑𝐹 β€œ dom 𝐻)))
61 inpreima 7034 . . . . . . . . . . . 12 (Fun 𝐹 β†’ (◑𝐹 β€œ (𝑒 ∩ dom 𝐻)) = ((◑𝐹 β€œ 𝑒) ∩ (◑𝐹 β€œ dom 𝐻)))
6220, 61syl 17 . . . . . . . . . . 11 (πœ‘ β†’ (◑𝐹 β€œ (𝑒 ∩ dom 𝐻)) = ((◑𝐹 β€œ 𝑒) ∩ (◑𝐹 β€œ dom 𝐻)))
6362adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ 𝐡) β†’ (◑𝐹 β€œ (𝑒 ∩ dom 𝐻)) = ((◑𝐹 β€œ 𝑒) ∩ (◑𝐹 β€œ dom 𝐻)))
645dmexd 7862 . . . . . . . . . . . . 13 (πœ‘ β†’ dom 𝐹 ∈ V)
65 restabs 22568 . . . . . . . . . . . . 13 ((𝑆 ∈ SAlg ∧ (◑𝐹 β€œ dom 𝐻) βŠ† dom 𝐹 ∧ dom 𝐹 ∈ V) β†’ ((𝑆 β†Ύt dom 𝐹) β†Ύt (◑𝐹 β€œ dom 𝐻)) = (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻)))
662, 4, 64, 65syl3anc 1371 . . . . . . . . . . . 12 (πœ‘ β†’ ((𝑆 β†Ύt dom 𝐹) β†Ύt (◑𝐹 β€œ dom 𝐻)) = (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻)))
6766eqcomd 2737 . . . . . . . . . . 11 (πœ‘ β†’ (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻)) = ((𝑆 β†Ύt dom 𝐹) β†Ύt (◑𝐹 β€œ dom 𝐻)))
6867adantr 481 . . . . . . . . . 10 ((πœ‘ ∧ 𝑒 ∈ 𝐡) β†’ (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻)) = ((𝑆 β†Ύt dom 𝐹) β†Ύt (◑𝐹 β€œ dom 𝐻)))
6960, 63, 683eltr4d 2847 . . . . . . . . 9 ((πœ‘ ∧ 𝑒 ∈ 𝐡) β†’ (◑𝐹 β€œ (𝑒 ∩ dom 𝐻)) ∈ (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻)))
70693adant3 1132 . . . . . . . 8 ((πœ‘ ∧ 𝑒 ∈ 𝐡 ∧ (◑𝐻 β€œ (-∞(,)π‘Ž)) = (𝑒 ∩ dom 𝐻)) β†’ (◑𝐹 β€œ (𝑒 ∩ dom 𝐻)) ∈ (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻)))
7147, 70eqeltrd 2832 . . . . . . 7 ((πœ‘ ∧ 𝑒 ∈ 𝐡 ∧ (◑𝐻 β€œ (-∞(,)π‘Ž)) = (𝑒 ∩ dom 𝐻)) β†’ (◑𝐹 β€œ (◑𝐻 β€œ (-∞(,)π‘Ž))) ∈ (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻)))
72713exp 1119 . . . . . 6 (πœ‘ β†’ (𝑒 ∈ 𝐡 β†’ ((◑𝐻 β€œ (-∞(,)π‘Ž)) = (𝑒 ∩ dom 𝐻) β†’ (◑𝐹 β€œ (◑𝐻 β€œ (-∞(,)π‘Ž))) ∈ (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻)))))
7372adantr 481 . . . . 5 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (𝑒 ∈ 𝐡 β†’ ((◑𝐻 β€œ (-∞(,)π‘Ž)) = (𝑒 ∩ dom 𝐻) β†’ (◑𝐹 β€œ (◑𝐻 β€œ (-∞(,)π‘Ž))) ∈ (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻)))))
7473rexlimdv 3152 . . . 4 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (βˆƒπ‘’ ∈ 𝐡 (◑𝐻 β€œ (-∞(,)π‘Ž)) = (𝑒 ∩ dom 𝐻) β†’ (◑𝐹 β€œ (◑𝐻 β€œ (-∞(,)π‘Ž))) ∈ (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻))))
7545, 74mpd 15 . . 3 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ (◑𝐹 β€œ (◑𝐻 β€œ (-∞(,)π‘Ž))) ∈ (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻)))
7632, 75eqeltrd 2832 . 2 ((πœ‘ ∧ π‘Ž ∈ ℝ) β†’ {π‘₯ ∈ (◑𝐹 β€œ dom 𝐻) ∣ ((𝐻 ∘ 𝐹)β€˜π‘₯) < π‘Ž} ∈ (𝑆 β†Ύt (◑𝐹 β€œ dom 𝐻)))
771, 2, 8, 23, 76issmfd 45129 1 (πœ‘ β†’ (𝐻 ∘ 𝐹) ∈ (SMblFnβ€˜π‘†))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106  βˆƒwrex 3069  {crab 3418  Vcvv 3459   ∩ cin 3927   βŠ† wss 3928  βˆͺ cuni 4885   class class class wbr 5125  β—‘ccnv 5652  dom cdm 5653  ran crn 5654   β€œ cima 5656   ∘ ccom 5657  Fun wfun 6510  βŸΆwf 6512  β€˜cfv 6516  (class class class)co 7377  β„cr 11074  -∞cmnf 11211  β„*cxr 11212   < clt 11213  (,)cioo 13289   β†Ύt crest 17331  topGenctg 17348  Topctop 22294  SAlgcsalg 44702  SalGencsalgen 44706  SMblFncsmblfn 45089
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5262  ax-sep 5276  ax-nul 5283  ax-pow 5340  ax-pr 5404  ax-un 7692  ax-inf2 9601  ax-cc 10395  ax-ac2 10423  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3364  df-reu 3365  df-rab 3419  df-v 3461  df-sbc 3758  df-csb 3874  df-dif 3931  df-un 3933  df-in 3935  df-ss 3945  df-pss 3947  df-nul 4303  df-if 4507  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4886  df-int 4928  df-iun 4976  df-iin 4977  df-br 5126  df-opab 5188  df-mpt 5209  df-tr 5243  df-id 5551  df-eprel 5557  df-po 5565  df-so 5566  df-fr 5608  df-se 5609  df-we 5610  df-xp 5659  df-rel 5660  df-cnv 5661  df-co 5662  df-dm 5663  df-rn 5664  df-res 5665  df-ima 5666  df-pred 6273  df-ord 6340  df-on 6341  df-lim 6342  df-suc 6343  df-iota 6468  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524  df-isom 6525  df-riota 7333  df-ov 7380  df-oprab 7381  df-mpo 7382  df-om 7823  df-1st 7941  df-2nd 7942  df-frecs 8232  df-wrecs 8263  df-recs 8337  df-rdg 8376  df-1o 8432  df-oadd 8436  df-omul 8437  df-er 8670  df-map 8789  df-pm 8790  df-en 8906  df-dom 8907  df-sdom 8908  df-fin 8909  df-sup 9402  df-inf 9403  df-oi 9470  df-card 9899  df-acn 9902  df-ac 10076  df-pnf 11215  df-mnf 11216  df-xr 11217  df-ltxr 11218  df-le 11219  df-sub 11411  df-neg 11412  df-div 11837  df-nn 12178  df-n0 12438  df-z 12524  df-uz 12788  df-q 12898  df-rp 12940  df-ioo 13293  df-ico 13295  df-fl 13722  df-rest 17333  df-topgen 17354  df-top 22295  df-bases 22348  df-salg 44703  df-salgen 44707  df-smblfn 45090
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator