Metamath Proof Explorer

Theorem sigaclci

Description: A sigma-algebra is closed under countable intersections. Deduction version. (Contributed by Thierry Arnoux, 19-Sep-2016)

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

Proof

Step Hyp Ref Expression
1 isrnsigau 
 |-  ( S e. U. ran sigAlgebra -> ( S C_ ~P U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
2 1 simprd 
 |-  ( S e. U. ran sigAlgebra -> ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) )
3 2 simp2d 
 |-  ( S e. U. ran sigAlgebra -> A. x e. S ( U. S \ x ) e. S )
4 3 adantr 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A. x e. S ( U. S \ x ) e. S )
5 elpwi 
 |-  ( A e. ~P S -> A C_ S )
6 ssrexv 
 |-  ( A C_ S -> ( E. z e. A y = ( U. S \ z ) -> E. z e. S y = ( U. S \ z ) ) )
7 5 6 syl 
 |-  ( A e. ~P S -> ( E. z e. A y = ( U. S \ z ) -> E. z e. S y = ( U. S \ z ) ) )
8 7 ss2abdv 
 |-  ( A e. ~P S -> { y | E. z e. A y = ( U. S \ z ) } C_ { y | E. z e. S y = ( U. S \ z ) } )
9 isrnsigau 
 |-  ( S e. U. ran sigAlgebra -> ( S C_ ~P U. S /\ ( U. S e. S /\ A. z e. S ( U. S \ z ) e. S /\ A. z e. ~P S ( z ~<_ _om -> U. z e. S ) ) ) )
10 9 simprd 
 |-  ( S e. U. ran sigAlgebra -> ( U. S e. S /\ A. z e. S ( U. S \ z ) e. S /\ A. z e. ~P S ( z ~<_ _om -> U. z e. S ) ) )
11 10 simp2d 
 |-  ( S e. U. ran sigAlgebra -> A. z e. S ( U. S \ z ) e. S )
12 uniiunlem 
 |-  ( A. z e. S ( U. S \ z ) e. S -> ( A. z e. S ( U. S \ z ) e. S <-> { y | E. z e. S y = ( U. S \ z ) } C_ S ) )
13 11 12 syl 
 |-  ( S e. U. ran sigAlgebra -> ( A. z e. S ( U. S \ z ) e. S <-> { y | E. z e. S y = ( U. S \ z ) } C_ S ) )
14 11 13 mpbid 
 |-  ( S e. U. ran sigAlgebra -> { y | E. z e. S y = ( U. S \ z ) } C_ S )
15 8 14 sylan9ssr 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> { y | E. z e. A y = ( U. S \ z ) } C_ S )
16 abrexexg 
 |-  ( A e. ~P S -> { y | E. z e. A y = ( U. S \ z ) } e. _V )
17 elpwg 
 |-  ( { y | E. z e. A y = ( U. S \ z ) } e. _V -> ( { y | E. z e. A y = ( U. S \ z ) } e. ~P S <-> { y | E. z e. A y = ( U. S \ z ) } C_ S ) )
18 16 17 syl 
 |-  ( A e. ~P S -> ( { y | E. z e. A y = ( U. S \ z ) } e. ~P S <-> { y | E. z e. A y = ( U. S \ z ) } C_ S ) )
19 18 adantl 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( { y | E. z e. A y = ( U. S \ z ) } e. ~P S <-> { y | E. z e. A y = ( U. S \ z ) } C_ S ) )
20 15 19 mpbird 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> { y | E. z e. A y = ( U. S \ z ) } e. ~P S )
21 2 simp3d 
 |-  ( S e. U. ran sigAlgebra -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
22 21 adantr 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
23 20 22 jca 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( { y | E. z e. A y = ( U. S \ z ) } e. ~P S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) )
24 abrexdom2jm 
 |-  ( A e. ~P S -> { y | E. z e. A y = ( U. S \ z ) } ~<_ A )
25 domtr 
 |-  ( ( { y | E. z e. A y = ( U. S \ z ) } ~<_ A /\ A ~<_ _om ) -> { y | E. z e. A y = ( U. S \ z ) } ~<_ _om )
26 24 25 sylan 
 |-  ( ( A e. ~P S /\ A ~<_ _om ) -> { y | E. z e. A y = ( U. S \ z ) } ~<_ _om )
27 26 ex 
 |-  ( A e. ~P S -> ( A ~<_ _om -> { y | E. z e. A y = ( U. S \ z ) } ~<_ _om ) )
28 27 adantl 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( A ~<_ _om -> { y | E. z e. A y = ( U. S \ z ) } ~<_ _om ) )
29 breq1 
 |-  ( x = { y | E. z e. A y = ( U. S \ z ) } -> ( x ~<_ _om <-> { y | E. z e. A y = ( U. S \ z ) } ~<_ _om ) )
30 unieq 
 |-  ( x = { y | E. z e. A y = ( U. S \ z ) } -> U. x = U. { y | E. z e. A y = ( U. S \ z ) } )
31 30 eleq1d 
 |-  ( x = { y | E. z e. A y = ( U. S \ z ) } -> ( U. x e. S <-> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) )
32 29 31 imbi12d 
 |-  ( x = { y | E. z e. A y = ( U. S \ z ) } -> ( ( x ~<_ _om -> U. x e. S ) <-> ( { y | E. z e. A y = ( U. S \ z ) } ~<_ _om -> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) ) )
33 32 rspcva 
 |-  ( ( { y | E. z e. A y = ( U. S \ z ) } e. ~P S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) -> ( { y | E. z e. A y = ( U. S \ z ) } ~<_ _om -> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) )
34 23 28 33 sylsyld 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( A ~<_ _om -> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) )
35 5 adantl 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A C_ S )
36 11 adantr 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A. z e. S ( U. S \ z ) e. S )
37 ssralv 
 |-  ( A C_ S -> ( A. z e. S ( U. S \ z ) e. S -> A. z e. A ( U. S \ z ) e. S ) )
38 35 36 37 sylc 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A. z e. A ( U. S \ z ) e. S )
39 dfiun2g 
 |-  ( A. z e. A ( U. S \ z ) e. S -> U_ z e. A ( U. S \ z ) = U. { y | E. z e. A y = ( U. S \ z ) } )
40 eleq1 
 |-  ( U_ z e. A ( U. S \ z ) = U. { y | E. z e. A y = ( U. S \ z ) } -> ( U_ z e. A ( U. S \ z ) e. S <-> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) )
41 38 39 40 3syl 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( U_ z e. A ( U. S \ z ) e. S <-> U. { y | E. z e. A y = ( U. S \ z ) } e. S ) )
42 34 41 sylibrd 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( A ~<_ _om -> U_ z e. A ( U. S \ z ) e. S ) )
43 difeq2 
 |-  ( x = U_ z e. A ( U. S \ z ) -> ( U. S \ x ) = ( U. S \ U_ z e. A ( U. S \ z ) ) )
44 43 eleq1d 
 |-  ( x = U_ z e. A ( U. S \ z ) -> ( ( U. S \ x ) e. S <-> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
45 44 rspccv 
 |-  ( A. x e. S ( U. S \ x ) e. S -> ( U_ z e. A ( U. S \ z ) e. S -> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
46 4 42 45 sylsyld 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( A ~<_ _om -> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
47 46 adantrd 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( ( A ~<_ _om /\ A =/= (/) ) -> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
48 47 imp 
 |-  ( ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) /\ ( A ~<_ _om /\ A =/= (/) ) ) -> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S )
49 simpr 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> A e. ~P S )
50 pwuni 
 |-  S C_ ~P U. S
51 5 50 sstrdi 
 |-  ( A e. ~P S -> A C_ ~P U. S )
52 iundifdifd 
 |-  ( A C_ ~P U. S -> ( A =/= (/) -> |^| A = ( U. S \ U_ z e. A ( U. S \ z ) ) ) )
53 49 51 52 3syl 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( A =/= (/) -> |^| A = ( U. S \ U_ z e. A ( U. S \ z ) ) ) )
54 53 adantld 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( ( A ~<_ _om /\ A =/= (/) ) -> |^| A = ( U. S \ U_ z e. A ( U. S \ z ) ) ) )
55 eleq1 
 |-  ( |^| A = ( U. S \ U_ z e. A ( U. S \ z ) ) -> ( |^| A e. S <-> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
56 54 55 syl6 
 |-  ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) -> ( ( A ~<_ _om /\ A =/= (/) ) -> ( |^| A e. S <-> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) ) )
57 56 imp 
 |-  ( ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) /\ ( A ~<_ _om /\ A =/= (/) ) ) -> ( |^| A e. S <-> ( U. S \ U_ z e. A ( U. S \ z ) ) e. S ) )
58 48 57 mpbird 
 |-  ( ( ( S e. U. ran sigAlgebra /\ A e. ~P S ) /\ ( A ~<_ _om /\ A =/= (/) ) ) -> |^| A e. S )