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 AA𝒫sigAlgebraOAsigAlgebraO

Proof

Step Hyp Ref Expression
1 intex AAV
2 1 biimpi AAV
3 2 adantr AA𝒫sigAlgebraOAV
4 intssuni AAA
5 4 adantr AA𝒫sigAlgebraOAA
6 simpr AA𝒫sigAlgebraOA𝒫sigAlgebraO
7 elpwi A𝒫sigAlgebraOAsigAlgebraO
8 sigasspw ssigAlgebraOs𝒫O
9 velpw s𝒫𝒫Os𝒫O
10 8 9 sylibr ssigAlgebraOs𝒫𝒫O
11 10 ssriv sigAlgebraO𝒫𝒫O
12 7 11 sstrdi A𝒫sigAlgebraOA𝒫𝒫O
13 6 12 syl AA𝒫sigAlgebraOA𝒫𝒫O
14 sspwuni A𝒫𝒫OA𝒫O
15 13 14 sylib AA𝒫sigAlgebraOA𝒫O
16 5 15 sstrd AA𝒫sigAlgebraOA𝒫O
17 simpr AA𝒫sigAlgebraOsAsA
18 simplr AA𝒫sigAlgebraOsAA𝒫sigAlgebraO
19 elelpwi sAA𝒫sigAlgebraOssigAlgebraO
20 17 18 19 syl2anc AA𝒫sigAlgebraOsAssigAlgebraO
21 vex sV
22 issiga sVssigAlgebraOs𝒫OOsxsOxsx𝒫sxωxs
23 21 22 ax-mp ssigAlgebraOs𝒫OOsxsOxsx𝒫sxωxs
24 20 23 sylib AA𝒫sigAlgebraOsAs𝒫OOsxsOxsx𝒫sxωxs
25 24 simprd AA𝒫sigAlgebraOsAOsxsOxsx𝒫sxωxs
26 25 simp1d AA𝒫sigAlgebraOsAOs
27 26 ralrimiva AA𝒫sigAlgebraOsAOs
28 n0 AssA
29 28 biimpi AssA
30 29 adantr AA𝒫sigAlgebraOssA
31 20 ex AA𝒫sigAlgebraOsAssigAlgebraO
32 31 eximdv AA𝒫sigAlgebraOssAsssigAlgebraO
33 30 32 mpd AA𝒫sigAlgebraOsssigAlgebraO
34 elfvex ssigAlgebraOOV
35 34 exlimiv sssigAlgebraOOV
36 33 35 syl AA𝒫sigAlgebraOOV
37 elintg OVOAsAOs
38 36 37 syl AA𝒫sigAlgebraOOAsAOs
39 27 38 mpbird AA𝒫sigAlgebraOOA
40 simpll AA𝒫sigAlgebraOxAsAAA𝒫sigAlgebraO
41 simpr AA𝒫sigAlgebraOxAsAsA
42 40 41 jca AA𝒫sigAlgebraOxAsAAA𝒫sigAlgebraOsA
43 elinti xAsAxs
44 43 imp xAsAxs
45 44 adantll AA𝒫sigAlgebraOxAsAxs
46 25 simp2d AA𝒫sigAlgebraOsAxsOxs
47 46 r19.21bi AA𝒫sigAlgebraOsAxsOxs
48 42 45 47 syl2anc AA𝒫sigAlgebraOxAsAOxs
49 48 ralrimiva AA𝒫sigAlgebraOxAsAOxs
50 36 difexd AA𝒫sigAlgebraOOxV
51 50 adantr AA𝒫sigAlgebraOxAOxV
52 elintg OxVOxAsAOxs
53 51 52 syl AA𝒫sigAlgebraOxAOxAsAOxs
54 49 53 mpbird AA𝒫sigAlgebraOxAOxA
55 54 ralrimiva AA𝒫sigAlgebraOxAOxA
56 simplll AA𝒫sigAlgebraOx𝒫AxωsAAA𝒫sigAlgebraO
57 simpr AA𝒫sigAlgebraOx𝒫AxωsAsA
58 56 57 jca AA𝒫sigAlgebraOx𝒫AxωsAAA𝒫sigAlgebraOsA
59 simpllr AA𝒫sigAlgebraOx𝒫AxωsAx𝒫A
60 elpwi x𝒫AxA
61 intss1 sAAs
62 60 61 sylan9ss x𝒫AsAxs
63 velpw x𝒫sxs
64 62 63 sylibr x𝒫AsAx𝒫s
65 59 64 sylancom AA𝒫sigAlgebraOx𝒫AxωsAx𝒫s
66 58 65 jca AA𝒫sigAlgebraOx𝒫AxωsAAA𝒫sigAlgebraOsAx𝒫s
67 simplr AA𝒫sigAlgebraOx𝒫AxωsAxω
68 25 simp3d AA𝒫sigAlgebraOsAx𝒫sxωxs
69 68 r19.21bi AA𝒫sigAlgebraOsAx𝒫sxωxs
70 66 67 69 sylc AA𝒫sigAlgebraOx𝒫AxωsAxs
71 70 ralrimiva AA𝒫sigAlgebraOx𝒫AxωsAxs
72 uniexg x𝒫AxV
73 72 ad2antlr AA𝒫sigAlgebraOx𝒫AxωxV
74 elintg xVxAsAxs
75 73 74 syl AA𝒫sigAlgebraOx𝒫AxωxAsAxs
76 71 75 mpbird AA𝒫sigAlgebraOx𝒫AxωxA
77 76 ex AA𝒫sigAlgebraOx𝒫AxωxA
78 77 ralrimiva AA𝒫sigAlgebraOx𝒫AxωxA
79 39 55 78 3jca AA𝒫sigAlgebraOOAxAOxAx𝒫AxωxA
80 issiga AVAsigAlgebraOA𝒫OOAxAOxAx𝒫AxωxA
81 80 biimpar AVA𝒫OOAxAOxAx𝒫AxωxAAsigAlgebraO
82 3 16 79 81 syl12anc AA𝒫sigAlgebraOAsigAlgebraO