Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  brsiga Unicode version

Theorem brsiga 23516
 Description: The Borel Algebra on real numbers is a Borel sigma algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
Assertion
Ref Expression
brsiga 𝔅 sigaGen

Proof of Theorem brsiga
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 retop 18272 . . 3
2 funmpt 5292 . . . . 5 sigAlgebra
3 df-sigagen 23502 . . . . . 6 sigaGen sigAlgebra
43funeqi 5277 . . . . 5 sigaGen sigAlgebra
52, 4mpbir 200 . . . 4 sigaGen
61elexi 2799 . . . . . 6
7 sigagensiga 23504 . . . . . 6 sigaGen sigAlgebra
8 issgon 23486 . . . . . . 7 sigaGen sigAlgebra sigaGen sigAlgebra sigaGen
98simplbi 446 . . . . . 6 sigaGen sigAlgebra sigaGen sigAlgebra
106, 7, 9mp2b 9 . . . . 5 sigaGen sigAlgebra
11 0elsiga 23477 . . . . 5 sigaGen sigAlgebra sigaGen
12 elfvdm 5556 . . . . 5 sigaGen sigaGen
1310, 11, 12mp2b 9 . . . 4 sigaGen
14 funfvima 5755 . . . 4 sigaGen sigaGen sigaGen sigaGen
155, 13, 14mp2an 653 . . 3 sigaGen sigaGen
161, 15ax-mp 8 . 2 sigaGen sigaGen
17 df-brsiga 23515 . . 3 𝔅 sigaGen
1817eleq1i 2348 . 2 𝔅 sigaGen sigaGen sigaGen
1916, 18mpbir 200 1 𝔅 sigaGen
 Colors of variables: wff set class Syntax hints:   wi 4   wceq 1625   wcel 1686  crab 2549  cvv 2790   wss 3154  c0 3457  cuni 3829  cint 3864   cmpt 4079   cdm 4691   crn 4692  cima 4694   wfun 5251  cfv 5257  cioo 10658  ctg 13344  ctop 16633  sigAlgebracsiga 23470  sigaGencsigagen 23501  𝔅ℝcbrsiga 23514 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-cnex 8795  ax-resscn 8796  ax-pre-lttri 8813  ax-pre-lttrn 8814 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-nel 2451  df-ral 2550  df-rex 2551  df-rab 2554  df-v 2792  df-sbc 2994  df-csb 3084  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-int 3865  df-iun 3909  df-br 4026  df-opab 4080  df-mpt 4081  df-id 4311  df-po 4316  df-so 4317  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-f1 5262  df-fo 5263  df-f1o 5264  df-fv 5265  df-ov 5863  df-oprab 5864  df-mpt2 5865  df-1st 6124  df-2nd 6125  df-er 6662  df-en 6866  df-dom 6867  df-sdom 6868  df-pnf 8871  df-mnf 8872  df-xr 8873  df-ltxr 8874  df-le 8875  df-ioo 10662  df-topgen 13346  df-top 16638  df-bases 16640  df-siga 23471  df-sigagen 23502  df-brsiga 23515
 Copyright terms: Public domain W3C validator