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 sseldi 
 |-  ( ( ( 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 ) )