Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  insiga Structured version   Visualization version   GIF version
Theorem insiga 32966
Description: The intersection of a collection of sigma-algebras of same base is a sigma-algebra. (Contributed by Thierry Arnoux, 27-Dec-2016.)
Assertion
Ref Expression
insiga ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ ∩ 𝐴 ∈ (sigAlgebraβ€˜π‘‚))
Proof of Theorem insiga
Dummy variables π‘₯ 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 intex 5330 . . . 4 (𝐴 β‰  βˆ… ↔ ∩ 𝐴 ∈ V)
21biimpi 215 . . 3 (𝐴 β‰  βˆ… β†’ ∩ 𝐴 ∈ V)
32adantr 481 . 2 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ ∩ 𝐴 ∈ V)
4 intssuni 4967 . . . 4 (𝐴 β‰  βˆ… β†’ ∩ 𝐴 βŠ† βˆͺ 𝐴)
54adantr 481 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ ∩ 𝐴 βŠ† βˆͺ 𝐴)
6 simpr 485 . . . . 5 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚))
7 elpwi 4603 . . . . . 6 (𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚) β†’ 𝐴 βŠ† (sigAlgebraβ€˜π‘‚))
8 sigasspw 32945 . . . . . . . 8 (𝑠 ∈ (sigAlgebraβ€˜π‘‚) β†’ 𝑠 βŠ† 𝒫 𝑂)
9 velpw 4601 . . . . . . . 8 (𝑠 ∈ 𝒫 𝒫 𝑂 ↔ 𝑠 βŠ† 𝒫 𝑂)
108, 9sylibr 233 . . . . . . 7 (𝑠 ∈ (sigAlgebraβ€˜π‘‚) β†’ 𝑠 ∈ 𝒫 𝒫 𝑂)
1110ssriv 3982 . . . . . 6 (sigAlgebraβ€˜π‘‚) βŠ† 𝒫 𝒫 𝑂
127, 11sstrdi 3990 . . . . 5 (𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚) β†’ 𝐴 βŠ† 𝒫 𝒫 𝑂)
136, 12syl 17 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ 𝐴 βŠ† 𝒫 𝒫 𝑂)
14 sspwuni 5096 . . . 4 (𝐴 βŠ† 𝒫 𝒫 𝑂 ↔ βˆͺ 𝐴 βŠ† 𝒫 𝑂)
1513, 14sylib 217 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ βˆͺ 𝐴 βŠ† 𝒫 𝑂)
165, 15sstrd 3988 . 2 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ ∩ 𝐴 βŠ† 𝒫 𝑂)
17 simpr 485 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ 𝐴)
18 simplr 767 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚))
19 elelpwi 4606 . . . . . . . . 9 ((𝑠 ∈ 𝐴 ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ 𝑠 ∈ (sigAlgebraβ€˜π‘‚))
2017, 18, 19syl2anc 584 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ (sigAlgebraβ€˜π‘‚))
21 vex 3477 . . . . . . . . 9 𝑠 ∈ V
22 issiga 32941 . . . . . . . . 9 (𝑠 ∈ V β†’ (𝑠 ∈ (sigAlgebraβ€˜π‘‚) ↔ (𝑠 βŠ† 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 (𝑂 βˆ– π‘₯) ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ 𝑠)))))
2321, 22ax-mp 5 . . . . . . . 8 (𝑠 ∈ (sigAlgebraβ€˜π‘‚) ↔ (𝑠 βŠ† 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 (𝑂 βˆ– π‘₯) ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ 𝑠))))
2420, 23sylib 217 . . . . . . 7 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ (𝑠 βŠ† 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 (𝑂 βˆ– π‘₯) ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ 𝑠))))
2524simprd 496 . . . . . 6 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ (𝑂 ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 (𝑂 βˆ– π‘₯) ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ 𝑠)))
2625simp1d 1142 . . . . 5 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ 𝑂 ∈ 𝑠)
2726ralrimiva 3145 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ βˆ€π‘  ∈ 𝐴 𝑂 ∈ 𝑠)
28 n0 4342 . . . . . . . . 9 (𝐴 β‰  βˆ… ↔ βˆƒπ‘  𝑠 ∈ 𝐴)
2928biimpi 215 . . . . . . . 8 (𝐴 β‰  βˆ… β†’ βˆƒπ‘  𝑠 ∈ 𝐴)
3029adantr 481 . . . . . . 7 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ βˆƒπ‘  𝑠 ∈ 𝐴)
3120ex 413 . . . . . . . 8 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ (𝑠 ∈ 𝐴 β†’ 𝑠 ∈ (sigAlgebraβ€˜π‘‚)))
3231eximdv 1920 . . . . . . 7 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ (βˆƒπ‘  𝑠 ∈ 𝐴 β†’ βˆƒπ‘  𝑠 ∈ (sigAlgebraβ€˜π‘‚)))
3330, 32mpd 15 . . . . . 6 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ βˆƒπ‘  𝑠 ∈ (sigAlgebraβ€˜π‘‚))
34 elfvex 6916 . . . . . . 7 (𝑠 ∈ (sigAlgebraβ€˜π‘‚) β†’ 𝑂 ∈ V)
3534exlimiv 1933 . . . . . 6 (βˆƒπ‘  𝑠 ∈ (sigAlgebraβ€˜π‘‚) β†’ 𝑂 ∈ V)
3633, 35syl 17 . . . . 5 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ 𝑂 ∈ V)
37 elintg 4951 . . . . 5 (𝑂 ∈ V β†’ (𝑂 ∈ ∩ 𝐴 ↔ βˆ€π‘  ∈ 𝐴 𝑂 ∈ 𝑠))
3836, 37syl 17 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ (𝑂 ∈ ∩ 𝐴 ↔ βˆ€π‘  ∈ 𝐴 𝑂 ∈ 𝑠))
3927, 38mpbird 256 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ 𝑂 ∈ ∩ 𝐴)
40 simpll 765 . . . . . . . 8 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) β†’ (𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)))
41 simpr 485 . . . . . . . 8 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ 𝐴)
4240, 41jca 512 . . . . . . 7 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) β†’ ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴))
43 elinti 4952 . . . . . . . . 9 (π‘₯ ∈ ∩ 𝐴 β†’ (𝑠 ∈ 𝐴 β†’ π‘₯ ∈ 𝑠))
4443imp 407 . . . . . . . 8 ((π‘₯ ∈ ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) β†’ π‘₯ ∈ 𝑠)
4544adantll 712 . . . . . . 7 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) β†’ π‘₯ ∈ 𝑠)
4625simp2d 1143 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ βˆ€π‘₯ ∈ 𝑠 (𝑂 βˆ– π‘₯) ∈ 𝑠)
4746r19.21bi 3247 . . . . . . 7 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) ∧ π‘₯ ∈ 𝑠) β†’ (𝑂 βˆ– π‘₯) ∈ 𝑠)
4842, 45, 47syl2anc 584 . . . . . 6 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) β†’ (𝑂 βˆ– π‘₯) ∈ 𝑠)
4948ralrimiva 3145 . . . . 5 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) β†’ βˆ€π‘  ∈ 𝐴 (𝑂 βˆ– π‘₯) ∈ 𝑠)
5036difexd 5322 . . . . . . 7 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ (𝑂 βˆ– π‘₯) ∈ V)
5150adantr 481 . . . . . 6 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) β†’ (𝑂 βˆ– π‘₯) ∈ V)
52 elintg 4951 . . . . . 6 ((𝑂 βˆ– π‘₯) ∈ V β†’ ((𝑂 βˆ– π‘₯) ∈ ∩ 𝐴 ↔ βˆ€π‘  ∈ 𝐴 (𝑂 βˆ– π‘₯) ∈ 𝑠))
5351, 52syl 17 . . . . 5 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) β†’ ((𝑂 βˆ– π‘₯) ∈ ∩ 𝐴 ↔ βˆ€π‘  ∈ 𝐴 (𝑂 βˆ– π‘₯) ∈ 𝑠))
5449, 53mpbird 256 . . . 4 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) β†’ (𝑂 βˆ– π‘₯) ∈ ∩ 𝐴)
5554ralrimiva 3145 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ βˆ€π‘₯ ∈ ∩ 𝐴(𝑂 βˆ– π‘₯) ∈ ∩ 𝐴)
56 simplll 773 . . . . . . . . . 10 (((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) ∧ 𝑠 ∈ 𝐴) β†’ (𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)))
57 simpr 485 . . . . . . . . . 10 (((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ 𝐴)
5856, 57jca 512 . . . . . . . . 9 (((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) ∧ 𝑠 ∈ 𝐴) β†’ ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴))
59 simpllr 774 . . . . . . . . . 10 (((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) ∧ 𝑠 ∈ 𝐴) β†’ π‘₯ ∈ 𝒫 ∩ 𝐴)
60 elpwi 4603 . . . . . . . . . . . 12 (π‘₯ ∈ 𝒫 ∩ 𝐴 β†’ π‘₯ βŠ† ∩ 𝐴)
61 intss1 4960 . . . . . . . . . . . 12 (𝑠 ∈ 𝐴 β†’ ∩ 𝐴 βŠ† 𝑠)
6260, 61sylan9ss 3991 . . . . . . . . . . 11 ((π‘₯ ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) β†’ π‘₯ βŠ† 𝑠)
63 velpw 4601 . . . . . . . . . . 11 (π‘₯ ∈ 𝒫 𝑠 ↔ π‘₯ βŠ† 𝑠)
6462, 63sylibr 233 . . . . . . . . . 10 ((π‘₯ ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) β†’ π‘₯ ∈ 𝒫 𝑠)
6559, 64sylancom 588 . . . . . . . . 9 (((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) ∧ 𝑠 ∈ 𝐴) β†’ π‘₯ ∈ 𝒫 𝑠)
6658, 65jca 512 . . . . . . . 8 (((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) ∧ 𝑠 ∈ 𝐴) β†’ (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) ∧ π‘₯ ∈ 𝒫 𝑠))
67 simplr 767 . . . . . . . 8 (((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) ∧ 𝑠 ∈ 𝐴) β†’ π‘₯ β‰Ό Ο‰)
6825simp3d 1144 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ βˆ€π‘₯ ∈ 𝒫 𝑠(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ 𝑠))
6968r19.21bi 3247 . . . . . . . 8 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ 𝑠))
7066, 67, 69sylc 65 . . . . . . 7 (((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) ∧ 𝑠 ∈ 𝐴) β†’ βˆͺ π‘₯ ∈ 𝑠)
7170ralrimiva 3145 . . . . . 6 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) β†’ βˆ€π‘  ∈ 𝐴 βˆͺ π‘₯ ∈ 𝑠)
72 uniexg 7713 . . . . . . . 8 (π‘₯ ∈ 𝒫 ∩ 𝐴 β†’ βˆͺ π‘₯ ∈ V)
7372ad2antlr 725 . . . . . . 7 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) β†’ βˆͺ π‘₯ ∈ V)
74 elintg 4951 . . . . . . 7 (βˆͺ π‘₯ ∈ V β†’ (βˆͺ π‘₯ ∈ ∩ 𝐴 ↔ βˆ€π‘  ∈ 𝐴 βˆͺ π‘₯ ∈ 𝑠))
7573, 74syl 17 . . . . . 6 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) β†’ (βˆͺ π‘₯ ∈ ∩ 𝐴 ↔ βˆ€π‘  ∈ 𝐴 βˆͺ π‘₯ ∈ 𝑠))
7671, 75mpbird 256 . . . . 5 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) β†’ βˆͺ π‘₯ ∈ ∩ 𝐴)
7776ex 413 . . . 4 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) β†’ (π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ ∩ 𝐴))
7877ralrimiva 3145 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ βˆ€π‘₯ ∈ 𝒫 ∩ 𝐴(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ ∩ 𝐴))
7939, 55, 783jca 1128 . 2 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ (𝑂 ∈ ∩ 𝐴 ∧ βˆ€π‘₯ ∈ ∩ 𝐴(𝑂 βˆ– π‘₯) ∈ ∩ 𝐴 ∧ βˆ€π‘₯ ∈ 𝒫 ∩ 𝐴(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ ∩ 𝐴)))
80 issiga 32941 . . 3 (∩ 𝐴 ∈ V β†’ (∩ 𝐴 ∈ (sigAlgebraβ€˜π‘‚) ↔ (∩ 𝐴 βŠ† 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ βˆ€π‘₯ ∈ ∩ 𝐴(𝑂 βˆ– π‘₯) ∈ ∩ 𝐴 ∧ βˆ€π‘₯ ∈ 𝒫 ∩ 𝐴(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ ∩ 𝐴)))))
8180biimpar 478 . 2 ((∩ 𝐴 ∈ V ∧ (∩ 𝐴 βŠ† 𝒫 𝑂 ∧ (𝑂 ∈ ∩ 𝐴 ∧ βˆ€π‘₯ ∈ ∩ 𝐴(𝑂 βˆ– π‘₯) ∈ ∩ 𝐴 ∧ βˆ€π‘₯ ∈ 𝒫 ∩ 𝐴(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ ∩ 𝐴)))) β†’ ∩ 𝐴 ∈ (sigAlgebraβ€˜π‘‚))
823, 16, 79, 81syl12anc 835 1 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ ∩ 𝐴 ∈ (sigAlgebraβ€˜π‘‚))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087  βˆƒwex 1781   ∈ wcel 2106   β‰  wne 2939  βˆ€wral 3060  Vcvv 3473   βˆ– cdif 3941   βŠ† wss 3944  βˆ…c0 4318  π’« cpw 4596  βˆͺ cuni 4901  βˆ© cint 4943   class class class wbr 5141  β€˜cfv 6532  Ο‰com 7838   β‰Ό cdom 8920  sigAlgebracsiga 32937
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5292  ax-nul 5299  ax-pow 5356  ax-pr 5420  ax-un 7708
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-nul 4319  df-if 4523  df-pw 4598  df-sn 4623  df-pr 4625  df-op 4629  df-uni 4902  df-int 4944  df-br 5142  df-opab 5204  df-mpt 5225  df-id 5567  df-xp 5675  df-rel 5676  df-cnv 5677  df-co 5678  df-dm 5679  df-iota 6484  df-fun 6534  df-fv 6540  df-siga 32938
This theorem is referenced by:  sigagensiga  32970
  Copyright terms: Public domain W3C validator