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 36 difexd 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> ( O \ x ) e. _V )
51 50 adantr 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. _V )
52 elintg 
 |-  ( ( O \ x ) e. _V -> ( ( O \ x ) e. |^| A <-> A. s e. A ( O \ x ) e. s ) )
53 51 52 syl 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( ( O \ x ) e. |^| A <-> A. s e. A ( O \ x ) e. s ) )
54 49 53 mpbird 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. |^| A ) -> ( O \ x ) e. |^| A )
55 54 ralrimiva 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> A. x e. |^| A ( O \ x ) e. |^| A )
56 simplll 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) )
57 simpr 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> s e. A )
58 56 57 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 ) )
59 simpllr 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> x e. ~P |^| A )
60 elpwi 
 |-  ( x e. ~P |^| A -> x C_ |^| A )
61 intss1 
 |-  ( s e. A -> |^| A C_ s )
62 60 61 sylan9ss 
 |-  ( ( x e. ~P |^| A /\ s e. A ) -> x C_ s )
63 velpw 
 |-  ( x e. ~P s <-> x C_ s )
64 62 63 sylibr 
 |-  ( ( x e. ~P |^| A /\ s e. A ) -> x e. ~P s )
65 59 64 sylancom 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> x e. ~P s )
66 58 65 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 ) )
67 simplr 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> x ~<_ _om )
68 25 simp3d 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) -> A. x e. ~P s ( x ~<_ _om -> U. x e. s ) )
69 68 r19.21bi 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ s e. A ) /\ x e. ~P s ) -> ( x ~<_ _om -> U. x e. s ) )
70 66 67 69 sylc 
 |-  ( ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) /\ s e. A ) -> U. x e. s )
71 70 ralrimiva 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) -> A. s e. A U. x e. s )
72 uniexg 
 |-  ( x e. ~P |^| A -> U. x e. _V )
73 72 ad2antlr 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) -> U. x e. _V )
74 elintg 
 |-  ( U. x e. _V -> ( U. x e. |^| A <-> A. s e. A U. x e. s ) )
75 73 74 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 ) )
76 71 75 mpbird 
 |-  ( ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) /\ x ~<_ _om ) -> U. x e. |^| A )
77 76 ex 
 |-  ( ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) /\ x e. ~P |^| A ) -> ( x ~<_ _om -> U. x e. |^| A ) )
78 77 ralrimiva 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> A. x e. ~P |^| A ( x ~<_ _om -> U. x e. |^| A ) )
79 39 55 78 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 ) ) )
80 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 ) ) ) ) )
81 80 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 ) )
82 3 16 79 81 syl12anc 
 |-  ( ( A =/= (/) /\ A e. ~P ( sigAlgebra ` O ) ) -> |^| A e. ( sigAlgebra ` O ) )