Metamath Proof Explorer


Theorem sigainb

Description: Building a sigma-algebra from intersections with a given set. (Contributed by Thierry Arnoux, 26-Dec-2016)

Ref Expression
Assertion sigainb
|- ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( S i^i ~P A ) e. ( sigAlgebra ` A ) )

Proof

Step Hyp Ref Expression
1 inex1g
 |-  ( S e. U. ran sigAlgebra -> ( S i^i ~P A ) e. _V )
2 1 adantr
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( S i^i ~P A ) e. _V )
3 inss2
 |-  ( S i^i ~P A ) C_ ~P A
4 3 a1i
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( S i^i ~P A ) C_ ~P A )
5 simpr
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A e. S )
6 pwidg
 |-  ( A e. S -> A e. ~P A )
7 5 6 syl
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A e. ~P A )
8 5 7 elind
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A e. ( S i^i ~P A ) )
9 simpll
 |-  ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> S e. U. ran sigAlgebra )
10 simplr
 |-  ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> A e. S )
11 inss1
 |-  ( S i^i ~P A ) C_ S
12 simpr
 |-  ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> x e. ( S i^i ~P A ) )
13 11 12 sselid
 |-  ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> x e. S )
14 difelsiga
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S /\ x e. S ) -> ( A \ x ) e. S )
15 9 10 13 14 syl3anc
 |-  ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> ( A \ x ) e. S )
16 difss
 |-  ( A \ x ) C_ A
17 elpwg
 |-  ( ( A \ x ) e. S -> ( ( A \ x ) e. ~P A <-> ( A \ x ) C_ A ) )
18 16 17 mpbiri
 |-  ( ( A \ x ) e. S -> ( A \ x ) e. ~P A )
19 15 18 syl
 |-  ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> ( A \ x ) e. ~P A )
20 15 19 elind
 |-  ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ( S i^i ~P A ) ) -> ( A \ x ) e. ( S i^i ~P A ) )
21 20 ralrimiva
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A. x e. ( S i^i ~P A ) ( A \ x ) e. ( S i^i ~P A ) )
22 simplll
 |-  ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> S e. U. ran sigAlgebra )
23 simplr
 |-  ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> x e. ~P ( S i^i ~P A ) )
24 elpwi
 |-  ( x e. ~P ( S i^i ~P A ) -> x C_ ( S i^i ~P A ) )
25 sstr
 |-  ( ( x C_ ( S i^i ~P A ) /\ ( S i^i ~P A ) C_ S ) -> x C_ S )
26 11 25 mpan2
 |-  ( x C_ ( S i^i ~P A ) -> x C_ S )
27 23 24 26 3syl
 |-  ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> x C_ S )
28 elpwg
 |-  ( x e. ~P ( S i^i ~P A ) -> ( x e. ~P S <-> x C_ S ) )
29 28 biimpar
 |-  ( ( x e. ~P ( S i^i ~P A ) /\ x C_ S ) -> x e. ~P S )
30 23 27 29 syl2anc
 |-  ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> x e. ~P S )
31 simpr
 |-  ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> x ~<_ _om )
32 sigaclcu
 |-  ( ( S e. U. ran sigAlgebra /\ x e. ~P S /\ x ~<_ _om ) -> U. x e. S )
33 22 30 31 32 syl3anc
 |-  ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> U. x e. S )
34 sstr
 |-  ( ( x C_ ( S i^i ~P A ) /\ ( S i^i ~P A ) C_ ~P A ) -> x C_ ~P A )
35 3 34 mpan2
 |-  ( x C_ ( S i^i ~P A ) -> x C_ ~P A )
36 23 24 35 3syl
 |-  ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> x C_ ~P A )
37 sspwuni
 |-  ( x C_ ~P A <-> U. x C_ A )
38 vuniex
 |-  U. x e. _V
39 38 elpw
 |-  ( U. x e. ~P A <-> U. x C_ A )
40 37 39 bitr4i
 |-  ( x C_ ~P A <-> U. x e. ~P A )
41 36 40 sylib
 |-  ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> U. x e. ~P A )
42 33 41 elind
 |-  ( ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) /\ x ~<_ _om ) -> U. x e. ( S i^i ~P A ) )
43 42 ex
 |-  ( ( ( S e. U. ran sigAlgebra /\ A e. S ) /\ x e. ~P ( S i^i ~P A ) ) -> ( x ~<_ _om -> U. x e. ( S i^i ~P A ) ) )
44 43 ralrimiva
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> A. x e. ~P ( S i^i ~P A ) ( x ~<_ _om -> U. x e. ( S i^i ~P A ) ) )
45 8 21 44 3jca
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( A e. ( S i^i ~P A ) /\ A. x e. ( S i^i ~P A ) ( A \ x ) e. ( S i^i ~P A ) /\ A. x e. ~P ( S i^i ~P A ) ( x ~<_ _om -> U. x e. ( S i^i ~P A ) ) ) )
46 issiga
 |-  ( ( S i^i ~P A ) e. _V -> ( ( S i^i ~P A ) e. ( sigAlgebra ` A ) <-> ( ( S i^i ~P A ) C_ ~P A /\ ( A e. ( S i^i ~P A ) /\ A. x e. ( S i^i ~P A ) ( A \ x ) e. ( S i^i ~P A ) /\ A. x e. ~P ( S i^i ~P A ) ( x ~<_ _om -> U. x e. ( S i^i ~P A ) ) ) ) ) )
47 46 biimpar
 |-  ( ( ( S i^i ~P A ) e. _V /\ ( ( S i^i ~P A ) C_ ~P A /\ ( A e. ( S i^i ~P A ) /\ A. x e. ( S i^i ~P A ) ( A \ x ) e. ( S i^i ~P A ) /\ A. x e. ~P ( S i^i ~P A ) ( x ~<_ _om -> U. x e. ( S i^i ~P A ) ) ) ) ) -> ( S i^i ~P A ) e. ( sigAlgebra ` A ) )
48 2 4 45 47 syl12anc
 |-  ( ( S e. U. ran sigAlgebra /\ A e. S ) -> ( S i^i ~P A ) e. ( sigAlgebra ` A ) )