Metamath Proof Explorer

Theorem sigaclcu

Description: A sigma-algebra is closed under countable union. (Contributed by Thierry Arnoux, 26-Dec-2016)

Ref Expression
Assertion sigaclcu 
|- ( ( S e. U. ran sigAlgebra /\ A e. ~P S /\ A ~<_ _om ) -> U. A e. S )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S /\ A ~<_ _om ) -> A e. ~P S )
2 isrnsiga 
 |-  ( S e. U. ran sigAlgebra <-> ( S e. _V /\ E. o ( S C_ ~P o /\ ( o e. S /\ A. x e. S ( o \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) ) )
3 2 simprbi 
 |-  ( S e. U. ran sigAlgebra -> E. o ( S C_ ~P o /\ ( o e. S /\ A. x e. S ( o \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
4 simpr3 
 |-  ( ( S C_ ~P o /\ ( o e. S /\ A. x e. S ( o \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
5 4 exlimiv 
 |-  ( E. o ( S C_ ~P o /\ ( o e. S /\ A. x e. S ( o \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
6 3 5 syl 
 |-  ( S e. U. ran sigAlgebra -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
7 6 3ad2ant1 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S /\ A ~<_ _om ) -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
8 simp3 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S /\ A ~<_ _om ) -> A ~<_ _om )
9 breq1 
 |-  ( x = A -> ( x ~<_ _om <-> A ~<_ _om ) )
10 unieq 
 |-  ( x = A -> U. x = U. A )
11 10 eleq1d 
 |-  ( x = A -> ( U. x e. S <-> U. A e. S ) )
12 9 11 imbi12d 
 |-  ( x = A -> ( ( x ~<_ _om -> U. x e. S ) <-> ( A ~<_ _om -> U. A e. S ) ) )
13 12 rspcv 
 |-  ( A e. ~P S -> ( A. x e. ~P S ( x ~<_ _om -> U. x e. S ) -> ( A ~<_ _om -> U. A e. S ) ) )
14 1 7 8 13 syl3c 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S /\ A ~<_ _om ) -> U. A e. S )