Theorem elrnsiga 34486

Description: Dropping the base information off a sigma-algebra. (Contributed by Thierry Arnoux, 13-Feb-2017.)

Assertion

Ref	Expression
elrnsiga	⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ ∪ ran sigAlgebra)

Proof of Theorem elrnsiga

Step	Hyp	Ref	Expression
1		fvssunirn 6916	. 2 ⊢ (sigAlgebra‘𝑂) ⊆ ∪ ran sigAlgebra
2	1	sseli 3941	1 ⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ ∪ ran sigAlgebra)

Syntax hints:   → wi 4   ∈ wcel 2150  ∪ cuni 4877  ran crn 5666  ‘cfv 6540  sigAlgebracsiga 34468

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2152  ax-9 2160  ax-10 2183  ax-12 2220  ax-ext 2742  ax-sep 5262  ax-nul 5274  ax-pr 5408

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1571  df-fal 1581  df-ex 1808  df-nf 1812  df-sb 2099  df-mo 2574  df-eu 2604  df-clab 2749  df-cleq 2762  df-clel 2845  df-ne 2966  df-rab 3424  df-v 3464  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-br 5115  df-opab 5179  df-cnv 5673  df-dm 5675  df-rn 5676  df-iota 6496  df-fv 6548

This theorem is referenced by:  sgsiga  34502  sigapisys  34515  sigaldsys  34519  brsiga  34543  sxsiga  34551  measinb2  34583  pwcntmeas  34587  ddemeas  34596  cnmbfm  34623  elmbfmvol2  34627  mbfmcnt  34628  br2base  34629  dya2iocbrsiga  34635  dya2icobrsiga  34636  sxbrsiga  34650  omsmeas  34683  isrrvv  34803  rrvadd  34812  rrvmulc  34813  dstrvprob  34832