Users' Mathboxes Mathbox for Glauco Siliprandi < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  intsaluni Structured version   Visualization version   Unicode version

Theorem intsaluni 38198
Description: The union of an arbitrary intersection of sigma-algebras on the same set  X, is  X. (Contributed by Glauco Siliprandi, 17-Aug-2020.)
Hypotheses
Ref Expression
intsaluni.ga  |-  ( ph  ->  G  C_ SAlg )
intsaluni.gn0  |-  ( ph  ->  G  =/=  (/) )
intsaluni.x  |-  ( (
ph  /\  s  e.  G )  ->  U. s  =  X )
Assertion
Ref Expression
intsaluni  |-  ( ph  ->  U. |^| G  =  X )
Distinct variable groups:    G, s    X, s    ph, s

Proof of Theorem intsaluni
Dummy variables  t  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 intsaluni.gn0 . . 3  |-  ( ph  ->  G  =/=  (/) )
2 n0 3743 . . . 4  |-  ( G  =/=  (/)  <->  E. s  s  e.  G )
32biimpi 198 . . 3  |-  ( G  =/=  (/)  ->  E. s 
s  e.  G )
41, 3syl 17 . 2  |-  ( ph  ->  E. s  s  e.  G )
5 nfv 1763 . . 3  |-  F/ s
ph
6 nfv 1763 . . 3  |-  F/ s U. |^| G  =  X
7 intss1 4252 . . . . . . . 8  |-  ( s  e.  G  ->  |^| G  C_  s )
8 uniss 4222 . . . . . . . 8  |-  ( |^| G  C_  s  ->  U. |^| G  C_  U. s )
97, 8syl 17 . . . . . . 7  |-  ( s  e.  G  ->  U. |^| G  C_  U. s )
109adantl 468 . . . . . 6  |-  ( (
ph  /\  s  e.  G )  ->  U. |^| G  C_  U. s )
11 intsaluni.x . . . . . 6  |-  ( (
ph  /\  s  e.  G )  ->  U. s  =  X )
1210, 11sseqtrd 3470 . . . . 5  |-  ( (
ph  /\  s  e.  G )  ->  U. |^| G  C_  X )
1311adantr 467 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  G )  /\  t  e.  G )  ->  U. s  =  X )
14 eleq1 2519 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  t  ->  (
s  e.  G  <->  t  e.  G ) )
1514anbi2d 711 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  t  ->  (
( ph  /\  s  e.  G )  <->  ( ph  /\  t  e.  G ) ) )
16 unieq 4209 . . . . . . . . . . . . . . . . . . 19  |-  ( s  =  t  ->  U. s  =  U. t )
1716eqeq1d 2455 . . . . . . . . . . . . . . . . . 18  |-  ( s  =  t  ->  ( U. s  =  X  <->  U. t  =  X ) )
1815, 17imbi12d 322 . . . . . . . . . . . . . . . . 17  |-  ( s  =  t  ->  (
( ( ph  /\  s  e.  G )  ->  U. s  =  X )  <->  ( ( ph  /\  t  e.  G )  ->  U. t  =  X ) ) )
1918, 11chvarv 2109 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  t  e.  G )  ->  U. t  =  X )
2019eqcomd 2459 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  G )  ->  X  =  U. t )
2120adantlr 722 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  s  e.  G )  /\  t  e.  G )  ->  X  =  U. t )
2213, 21eqtrd 2487 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  s  e.  G )  /\  t  e.  G )  ->  U. s  =  U. t )
23 intsaluni.ga . . . . . . . . . . . . . . . 16  |-  ( ph  ->  G  C_ SAlg )
2423sselda 3434 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  t  e.  G )  ->  t  e. SAlg )
25 saluni 38195 . . . . . . . . . . . . . . 15  |-  ( t  e. SAlg  ->  U. t  e.  t )
2624, 25syl 17 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  t  e.  G )  ->  U. t  e.  t )
2726adantlr 722 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  s  e.  G )  /\  t  e.  G )  ->  U. t  e.  t )
2822, 27eqeltrd 2531 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  s  e.  G )  /\  t  e.  G )  ->  U. s  e.  t )
2928ralrimiva 2804 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  G )  ->  A. t  e.  G  U. s  e.  t )
30 uniexg 6593 . . . . . . . . . . . . 13  |-  ( s  e.  G  ->  U. s  e.  _V )
3130adantl 468 . . . . . . . . . . . 12  |-  ( (
ph  /\  s  e.  G )  ->  U. s  e.  _V )
32 elintg 4245 . . . . . . . . . . . 12  |-  ( U. s  e.  _V  ->  ( U. s  e.  |^| G 
<-> 
A. t  e.  G  U. s  e.  t
) )
3331, 32syl 17 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  G )  ->  ( U. s  e.  |^| G  <->  A. t  e.  G  U. s  e.  t )
)
3429, 33mpbird 236 . . . . . . . . . 10  |-  ( (
ph  /\  s  e.  G )  ->  U. s  e.  |^| G )
3534adantr 467 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  G )  /\  x  e.  X )  ->  U. s  e.  |^| G )
36 simpr 463 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  G )  /\  x  e.  X )  ->  x  e.  X )
3711eqcomd 2459 . . . . . . . . . . 11  |-  ( (
ph  /\  s  e.  G )  ->  X  =  U. s )
3837adantr 467 . . . . . . . . . 10  |-  ( ( ( ph  /\  s  e.  G )  /\  x  e.  X )  ->  X  =  U. s )
3936, 38eleqtrd 2533 . . . . . . . . 9  |-  ( ( ( ph  /\  s  e.  G )  /\  x  e.  X )  ->  x  e.  U. s )
40 eleq2 2520 . . . . . . . . . 10  |-  ( y  =  U. s  -> 
( x  e.  y  <-> 
x  e.  U. s
) )
4140rspcev 3152 . . . . . . . . 9  |-  ( ( U. s  e.  |^| G  /\  x  e.  U. s )  ->  E. y  e.  |^| G x  e.  y )
4235, 39, 41syl2anc 667 . . . . . . . 8  |-  ( ( ( ph  /\  s  e.  G )  /\  x  e.  X )  ->  E. y  e.  |^| G x  e.  y )
43 eluni2 4205 . . . . . . . 8  |-  ( x  e.  U. |^| G  <->  E. y  e.  |^| G x  e.  y )
4442, 43sylibr 216 . . . . . . 7  |-  ( ( ( ph  /\  s  e.  G )  /\  x  e.  X )  ->  x  e.  U. |^| G )
4544ralrimiva 2804 . . . . . 6  |-  ( (
ph  /\  s  e.  G )  ->  A. x  e.  X  x  e.  U.
|^| G )
46 dfss3 3424 . . . . . 6  |-  ( X 
C_  U. |^| G  <->  A. x  e.  X  x  e.  U.
|^| G )
4745, 46sylibr 216 . . . . 5  |-  ( (
ph  /\  s  e.  G )  ->  X  C_ 
U. |^| G )
4812, 47eqssd 3451 . . . 4  |-  ( (
ph  /\  s  e.  G )  ->  U. |^| G  =  X )
4948ex 436 . . 3  |-  ( ph  ->  ( s  e.  G  ->  U. |^| G  =  X ) )
505, 6, 49exlimd 1999 . 2  |-  ( ph  ->  ( E. s  s  e.  G  ->  U. |^| G  =  X )
)
514, 50mpd 15 1  |-  ( ph  ->  U. |^| G  =  X )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    /\ wa 371    = wceq 1446   E.wex 1665    e. wcel 1889    =/= wne 2624   A.wral 2739   E.wrex 2740   _Vcvv 3047    C_ wss 3406   (/)c0 3733   U.cuni 4201   |^|cint 4237  SAlgcsalg 38179
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-8 1891  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-un 6588
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-ral 2744  df-rex 2745  df-rab 2748  df-v 3049  df-dif 3409  df-in 3413  df-ss 3420  df-nul 3734  df-pw 3955  df-uni 4202  df-int 4238  df-salg 38180
This theorem is referenced by:  intsal  38199  salgenuni  38206
  Copyright terms: Public domain W3C validator