Metamath Proof Explorer

Theorem insiga

Description: The intersection of a collection of sigma-algebras of same base is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016)

Ref Expression
Assertion insiga 
|- ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> |^| A e. ( sigAlgebra ` O ) )

Proof

Step Hyp Ref Expression
1 intex 
 |-  ( A =/= (/) <-> |^| A e. _V )
2 1 birani 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> |^| A e. _V )
3 intssuni 
 |-  ( A =/= (/) -> |^| A C_ U. A )
4 3 adantr 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> |^| A C_ U. A )
5 simpr 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> A e. ~P ( sigAlgebra ` O ) )
6 elpwi 
 |-  ( A e. ~P ( sigAlgebra ` O ) -> A C_ ( sigAlgebra ` O ) )
7 sigasspw 
 |-  ( s e. ( sigAlgebra ` O ) -> s C_ ~P O )
8 velpw 
 |-  ( s e. ~P ~P O <-> s C_ ~P O )
9 7 8 sylibr 
 |-  ( s e. ( sigAlgebra ` O ) -> s e. ~P ~P O )
10 9 ssriv 
 |-  ( sigAlgebra ` O ) C_ ~P ~P O
11 6 10 sstrdi 
 |-  ( A e. ~P ( sigAlgebra ` O ) -> A C_ ~P ~P O )
12 5 11 syl 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> A C_ ~P ~P O )
13 sspwuni 
 |-  ( A C_ ~P ~P O <-> U. A C_ ~P O )
14 12 13 sylib 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> U. A C_ ~P O )
15 4 14 sstrd 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> |^| A C_ ~P O )
16 simpr 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) -> s e. A )
17 simplr 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) -> A e. ~P ( sigAlgebra ` O ) )
18 elelpwi 
 |-  ( ( s e. A /\ A e. ~P ( sigAlgebra ` O ) ) -> s e. ( sigAlgebra ` O ) )
19 16 17 18 syl2anc 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) -> s e. ( sigAlgebra ` O ) )
20 vex 
 |-  s e. _V
21 issiga 
 |-  ( s e. _V -> ( s e. ( sigAlgebra ` 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 ) ) ) ) )
22 20 21 ax-mp 
 |-  ( s e. ( sigAlgebra ` 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 ) ) ) )
23 19 22 sylib 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) -> ( 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 ) ) ) )
24 23 simprd 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) -> ( O e. s /\ A. x e. s ( O \ x ) e. s /\ A. x e. ~P s ( x ~<_ _om -> U. x e. s ) ) )
25 24 simp1d 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) -> O e. s )
26 25 ralrimiva 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> A. s e. A O e. s )
27 n0 
 |-  ( A =/= (/) <-> E. s s e. A )
28 27 birani 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> E. s s e. A )
29 19 ex 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> ( s e. A -> s e. ( sigAlgebra ` O ) ) )
30 29 eximdv 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> ( E. s s e. A -> E. s s e. ( sigAlgebra ` O ) ) )
31 28 30 mpd 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> E. s s e. ( sigAlgebra ` O ) )
32 elfvex 
 |-  ( s e. ( sigAlgebra ` O ) -> O e. _V )
33 32 exlimiv 
 |-  ( E. s s e. ( sigAlgebra ` O ) -> O e. _V )
34 31 33 syl 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> O e. _V )
35 elintg 
 |-  ( O e. _V -> ( O e. |^| A <-> A. s e. A O e. s ) )
36 34 35 syl 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> ( O e. |^| A <-> A. s e. A O e. s ) )
37 26 36 mpbird 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> O e. |^| A )
38 simpll 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) )
39 simpr 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> s e. A )
40 38 39 jca 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) )
41 elinti 
 |-  ( x e. |^| A -> ( s e. A -> x e. s ) )
42 41 imp 
 |-  ( ( x e. |^| A /\ s e. A ) -> x e. s )
43 42 adantll 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> x e. s )
44 24 simp2d 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) -> A. x e. s ( O \ x ) e. s )
45 44 r19.21bi 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) /\ x e. s ) -> ( O \ x ) e. s )
46 40 43 45 syl2anc 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) /\ s e. A ) -> ( O \ x ) e. s )
47 46 ralrimiva 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) -> A. s e. A ( O \ x ) e. s )
48 34 difexd 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> ( O \ x ) e. _V )
49 48 adantr 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. _V )
50 elintg 
 |-  ( ( O \ x ) e. _V -> ( ( O \ x ) e. |^| A <-> A. s e. A ( O \ x ) e. s ) )
51 49 50 syl 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( ( O \ x ) e. |^| A <-> A. s e. A ( O \ x ) e. s ) )
52 47 51 mpbird 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. |^| A )
53 52 ralrimiva 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> A. x e. |^| A ( O \ x ) e. |^| A )
54 simplll 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) )
55 simpr 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> s e. A )
56 54 55 jca 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) )
57 simpllr 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> x e. ~P |^| A )
58 elpwi 
 |-  ( x e. ~P |^| A -> x C_ |^| A )
59 intss1 
 |-  ( s e. A -> |^| A C_ s )
60 58 59 sylan9ss 
 |-  ( ( x e. ~P |^| A /\ s e. A ) -> x C_ s )
61 velpw 
 |-  ( x e. ~P s <-> x C_ s )
62 60 61 sylibr 
 |-  ( ( x e. ~P |^| A /\ s e. A ) -> x e. ~P s )
63 57 62 sylancom 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> x e. ~P s )
64 56 63 jca 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) /\ x e. ~P s ) )
65 simplr 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> x ~<_ _om )
66 24 simp3d 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) -> A. x e. ~P s ( x ~<_ _om -> U. x e. s ) )
67 66 r19.21bi 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) /\ x e. ~P s ) -> ( x ~<_ _om -> U. x e. s ) )
68 64 65 67 sylc 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> U. x e. s )
69 68 ralrimiva 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) -> A. s e. A U. x e. s )
70 uniexg 
 |-  ( x e. ~P |^| A -> U. x e. _V )
71 70 ad2antlr 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) -> U. x e. _V )
72 elintg 
 |-  ( U. x e. _V -> ( U. x e. |^| A <-> A. s e. A U. x e. s ) )
73 71 72 syl 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) -> ( U. x e. |^| A <-> A. s e. A U. x e. s ) )
74 69 73 mpbird 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) -> U. x e. |^| A )
75 74 ex 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) -> ( x ~<_ _om -> U. x e. |^| A ) )
76 75 ralrimiva 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> A. x e. ~P |^| A ( x ~<_ _om -> U. x e. |^| A ) )
77 37 53 76 3jca 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> ( O e. |^| A /\ A. x e. |^| A ( O \ x ) e. |^| A /\ A. x e. ~P |^| A ( x ~<_ _om -> U. x e. |^| A ) ) )
78 issiga 
 |-  ( |^| A e. _V -> ( |^| A e. ( sigAlgebra ` O ) <-> ( |^| A C_ ~P O /\ ( O e. |^| A /\ A. x e. |^| A ( O \ x ) e. |^| A /\ A. x e. ~P |^| A ( x ~<_ _om -> U. x e. |^| A ) ) ) ) )
79 78 biimpar 
 |-  ( ( |^| A e. _V /\ ( |^| A C_ ~P O /\ ( O e. |^| A /\ A. x e. |^| A ( O \ x ) e. |^| A /\ A. x e. ~P |^| A ( x ~<_ _om -> U. x e. |^| A ) ) ) ) -> |^| A e. ( sigAlgebra ` O ) )
80 2 15 77 79 syl12anc 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> |^| A e. ( sigAlgebra ` O ) )