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 32605
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 5292 . . . 4 (𝐴 β‰  βˆ… ↔ ∩ 𝐴 ∈ V)
21biimpi 215 . . 3 (𝐴 β‰  βˆ… β†’ ∩ 𝐴 ∈ V)
32adantr 481 . 2 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ ∩ 𝐴 ∈ V)
4 intssuni 4929 . . . 4 (𝐴 β‰  βˆ… β†’ ∩ 𝐴 βŠ† βˆͺ 𝐴)
54adantr 481 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ ∩ 𝐴 βŠ† βˆͺ 𝐴)
6 simpr 485 . . . . 5 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚))
7 elpwi 4565 . . . . . 6 (𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚) β†’ 𝐴 βŠ† (sigAlgebraβ€˜π‘‚))
8 sigasspw 32584 . . . . . . . 8 (𝑠 ∈ (sigAlgebraβ€˜π‘‚) β†’ 𝑠 βŠ† 𝒫 𝑂)
9 velpw 4563 . . . . . . . 8 (𝑠 ∈ 𝒫 𝒫 𝑂 ↔ 𝑠 βŠ† 𝒫 𝑂)
108, 9sylibr 233 . . . . . . 7 (𝑠 ∈ (sigAlgebraβ€˜π‘‚) β†’ 𝑠 ∈ 𝒫 𝒫 𝑂)
1110ssriv 3946 . . . . . 6 (sigAlgebraβ€˜π‘‚) βŠ† 𝒫 𝒫 𝑂
127, 11sstrdi 3954 . . . . 5 (𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚) β†’ 𝐴 βŠ† 𝒫 𝒫 𝑂)
136, 12syl 17 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ 𝐴 βŠ† 𝒫 𝒫 𝑂)
14 sspwuni 5058 . . . 4 (𝐴 βŠ† 𝒫 𝒫 𝑂 ↔ βˆͺ 𝐴 βŠ† 𝒫 𝑂)
1513, 14sylib 217 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ βˆͺ 𝐴 βŠ† 𝒫 𝑂)
165, 15sstrd 3952 . 2 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ ∩ 𝐴 βŠ† 𝒫 𝑂)
17 simpr 485 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ 𝐴)
18 simplr 767 . . . . . . . . 9 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚))
19 elelpwi 4568 . . . . . . . . 9 ((𝑠 ∈ 𝐴 ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ 𝑠 ∈ (sigAlgebraβ€˜π‘‚))
2017, 18, 19syl2anc 584 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ 𝑠 ∈ (sigAlgebraβ€˜π‘‚))
21 vex 3447 . . . . . . . . 9 𝑠 ∈ V
22 issiga 32580 . . . . . . . . 9 (𝑠 ∈ V β†’ (𝑠 ∈ (sigAlgebraβ€˜π‘‚) ↔ (𝑠 βŠ† 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 (𝑂 βˆ– π‘₯) ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ 𝑠)))))
2321, 22ax-mp 5 . . . . . . . 8 (𝑠 ∈ (sigAlgebraβ€˜π‘‚) ↔ (𝑠 βŠ† 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 (𝑂 βˆ– π‘₯) ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ 𝑠))))
2420, 23sylib 217 . . . . . . 7 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ (𝑠 βŠ† 𝒫 𝑂 ∧ (𝑂 ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 (𝑂 βˆ– π‘₯) ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ 𝑠))))
2524simprd 496 . . . . . 6 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ (𝑂 ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 (𝑂 βˆ– π‘₯) ∈ 𝑠 ∧ βˆ€π‘₯ ∈ 𝒫 𝑠(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ 𝑠)))
2625simp1d 1142 . . . . 5 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ 𝑂 ∈ 𝑠)
2726ralrimiva 3141 . . . 4 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ βˆ€π‘  ∈ 𝐴 𝑂 ∈ 𝑠)
28 n0 4304 . . . . . . . . 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 6877 . . . . . . 7 (𝑠 ∈ (sigAlgebraβ€˜π‘‚) β†’ 𝑂 ∈ V)
3534exlimiv 1933 . . . . . 6 (βˆƒπ‘  𝑠 ∈ (sigAlgebraβ€˜π‘‚) β†’ 𝑂 ∈ V)
3633, 35syl 17 . . . . 5 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ 𝑂 ∈ V)
37 elintg 4913 . . . . 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 4914 . . . . . . . . 9 (π‘₯ ∈ ∩ 𝐴 β†’ (𝑠 ∈ 𝐴 β†’ π‘₯ ∈ 𝑠))
4443imp 407 . . . . . . . 8 ((π‘₯ ∈ ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) β†’ π‘₯ ∈ 𝑠)
4544adantll 712 . . . . . . 7 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) β†’ π‘₯ ∈ 𝑠)
4625simp2d 1143 . . . . . . . 8 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) β†’ βˆ€π‘₯ ∈ 𝑠 (𝑂 βˆ– π‘₯) ∈ 𝑠)
4746r19.21bi 3232 . . . . . . 7 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) ∧ π‘₯ ∈ 𝑠) β†’ (𝑂 βˆ– π‘₯) ∈ 𝑠)
4842, 45, 47syl2anc 584 . . . . . 6 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) ∧ 𝑠 ∈ 𝐴) β†’ (𝑂 βˆ– π‘₯) ∈ 𝑠)
4948ralrimiva 3141 . . . . 5 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) β†’ βˆ€π‘  ∈ 𝐴 (𝑂 βˆ– π‘₯) ∈ 𝑠)
5036difexd 5284 . . . . . . 7 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ (𝑂 βˆ– π‘₯) ∈ V)
5150adantr 481 . . . . . 6 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) β†’ (𝑂 βˆ– π‘₯) ∈ V)
52 elintg 4913 . . . . . 6 ((𝑂 βˆ– π‘₯) ∈ V β†’ ((𝑂 βˆ– π‘₯) ∈ ∩ 𝐴 ↔ βˆ€π‘  ∈ 𝐴 (𝑂 βˆ– π‘₯) ∈ 𝑠))
5351, 52syl 17 . . . . 5 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) β†’ ((𝑂 βˆ– π‘₯) ∈ ∩ 𝐴 ↔ βˆ€π‘  ∈ 𝐴 (𝑂 βˆ– π‘₯) ∈ 𝑠))
5449, 53mpbird 256 . . . 4 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ ∩ 𝐴) β†’ (𝑂 βˆ– π‘₯) ∈ ∩ 𝐴)
5554ralrimiva 3141 . . 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 4565 . . . . . . . . . . . 12 (π‘₯ ∈ 𝒫 ∩ 𝐴 β†’ π‘₯ βŠ† ∩ 𝐴)
61 intss1 4922 . . . . . . . . . . . 12 (𝑠 ∈ 𝐴 β†’ ∩ 𝐴 βŠ† 𝑠)
6260, 61sylan9ss 3955 . . . . . . . . . . 11 ((π‘₯ ∈ 𝒫 ∩ 𝐴 ∧ 𝑠 ∈ 𝐴) β†’ π‘₯ βŠ† 𝑠)
63 velpw 4563 . . . . . . . . . . 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 3232 . . . . . . . 8 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ 𝑠 ∈ 𝐴) ∧ π‘₯ ∈ 𝒫 𝑠) β†’ (π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ 𝑠))
7066, 67, 69sylc 65 . . . . . . 7 (((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) ∧ 𝑠 ∈ 𝐴) β†’ βˆͺ π‘₯ ∈ 𝑠)
7170ralrimiva 3141 . . . . . 6 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) β†’ βˆ€π‘  ∈ 𝐴 βˆͺ π‘₯ ∈ 𝑠)
72 uniexg 7673 . . . . . . . 8 (π‘₯ ∈ 𝒫 ∩ 𝐴 β†’ βˆͺ π‘₯ ∈ V)
7372ad2antlr 725 . . . . . . 7 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) β†’ βˆͺ π‘₯ ∈ V)
74 elintg 4913 . . . . . . 7 (βˆͺ π‘₯ ∈ V β†’ (βˆͺ π‘₯ ∈ ∩ 𝐴 ↔ βˆ€π‘  ∈ 𝐴 βˆͺ π‘₯ ∈ 𝑠))
7573, 74syl 17 . . . . . 6 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) β†’ (βˆͺ π‘₯ ∈ ∩ 𝐴 ↔ βˆ€π‘  ∈ 𝐴 βˆͺ π‘₯ ∈ 𝑠))
7671, 75mpbird 256 . . . . 5 ((((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) ∧ π‘₯ β‰Ό Ο‰) β†’ βˆͺ π‘₯ ∈ ∩ 𝐴)
7776ex 413 . . . 4 (((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) ∧ π‘₯ ∈ 𝒫 ∩ 𝐴) β†’ (π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ ∩ 𝐴))
7877ralrimiva 3141 . . 3 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ βˆ€π‘₯ ∈ 𝒫 ∩ 𝐴(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ ∩ 𝐴))
7939, 55, 783jca 1128 . 2 ((𝐴 β‰  βˆ… ∧ 𝐴 ∈ 𝒫 (sigAlgebraβ€˜π‘‚)) β†’ (𝑂 ∈ ∩ 𝐴 ∧ βˆ€π‘₯ ∈ ∩ 𝐴(𝑂 βˆ– π‘₯) ∈ ∩ 𝐴 ∧ βˆ€π‘₯ ∈ 𝒫 ∩ 𝐴(π‘₯ β‰Ό Ο‰ β†’ βˆͺ π‘₯ ∈ ∩ 𝐴)))
80 issiga 32580 . . 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 2941  βˆ€wral 3062  Vcvv 3443   βˆ– cdif 3905   βŠ† wss 3908  βˆ…c0 4280  π’« cpw 4558  βˆͺ cuni 4863  βˆ© cint 4905   class class class wbr 5103  β€˜cfv 6493  Ο‰com 7798   β‰Ό cdom 8877  sigAlgebracsiga 32576
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 2707  ax-sep 5254  ax-nul 5261  ax-pow 5318  ax-pr 5382  ax-un 7668
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 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2887  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3406  df-v 3445  df-sbc 3738  df-csb 3854  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4281  df-if 4485  df-pw 4560  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4864  df-int 4906  df-br 5104  df-opab 5166  df-mpt 5187  df-id 5529  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-iota 6445  df-fun 6495  df-fv 6501  df-siga 32577
This theorem is referenced by:  sigagensiga  32609
  Copyright terms: Public domain W3C validator