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