Theorem elrnsiga 34623

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 6913	. 2 ⊢ (sigAlgebra‘𝑂) ⊆ ∪ ran sigAlgebra
2	1	sseli 3930	1 ⊢ (𝑆 ∈ (sigAlgebra‘𝑂) → 𝑆 ∈ ∪ ran sigAlgebra)

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145  ∪ cuni 4870  ran crn 5660  ‘cfv 6537  sigAlgebracsiga 34605

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-12 2215  ax-ext 2734  ax-sep 5255  ax-nul 5267  ax-pr 5402

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-rab 3415  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-br 5108  df-opab 5172  df-cnv 5667  df-dm 5669  df-rn 5670  df-iota 6493  df-fv 6545

This theorem is used by:  sgsiga  34640  sigapisys  34653  sigaldsys  34657  brsiga  34681  sxsiga  34689  measinb2  34721  pwcntmeas  34725  ddemeas  34734  cnmbfm  34761  elmbfmvol2  34765  mbfmcnt  34766  br2base  34767  dya2iocbrsiga  34773  dya2icobrsiga  34774  sxbrsiga  34788  omsmeas  34821  isrrvv  34941  rrvadd  34950  rrvmulc  34951  dstrvprob  34970