Metamath Proof Explorer

Theorem intsal

Description: The arbitrary intersection of sigma-algebra (on the same set X ) is a sigma-algebra ( on the same set X , see intsaluni ). (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses intsal.ga 
|- ( ph -> G C_ SAlg )
intsal.gn0 
|- ( ph -> G =/= (/) )
intsal.x 
|- ( ( ph /\ s e. G ) -> U. s = X )
Assertion intsal 
|- ( ph -> |^| G e. SAlg )

Proof

Step Hyp Ref Expression
1 intsal.ga 
 |-  ( ph -> G C_ SAlg )
2 intsal.gn0 
 |-  ( ph -> G =/= (/) )
3 intsal.x 
 |-  ( ( ph /\ s e. G ) -> U. s = X )
4 simpl 
 |-  ( ( ph /\ s e. G ) -> ph )
5 1 sselda 
 |-  ( ( ph /\ s e. G ) -> s e. SAlg )
6 simpr 
 |-  ( ( ph /\ s e. SAlg ) -> s e. SAlg )
7 0sal 
 |-  ( s e. SAlg -> (/) e. s )
8 6 7 syl 
 |-  ( ( ph /\ s e. SAlg ) -> (/) e. s )
9 4 5 8 syl2anc 
 |-  ( ( ph /\ s e. G ) -> (/) e. s )
10 9 ralrimiva 
 |-  ( ph -> A. s e. G (/) e. s )
11 0ex 
 |-  (/) e. _V
12 11 elint2 
 |-  ( (/) e. |^| G <-> A. s e. G (/) e. s )
13 10 12 sylibr 
 |-  ( ph -> (/) e. |^| G )
14 1 2 3 intsaluni 
 |-  ( ph -> U. |^| G = X )
15 14 eqcomd 
 |-  ( ph -> X = U. |^| G )
16 15 adantr 
 |-  ( ( ph /\ s e. G ) -> X = U. |^| G )
17 3 16 eqtr2d 
 |-  ( ( ph /\ s e. G ) -> U. |^| G = U. s )
18 17 difeq1d 
 |-  ( ( ph /\ s e. G ) -> ( U. |^| G \ y ) = ( U. s \ y ) )
19 18 adantlr 
 |-  ( ( ( ph /\ y e. |^| G ) /\ s e. G ) -> ( U. |^| G \ y ) = ( U. s \ y ) )
20 5 adantlr 
 |-  ( ( ( ph /\ y e. |^| G ) /\ s e. G ) -> s e. SAlg )
21 elinti 
 |-  ( y e. |^| G -> ( s e. G -> y e. s ) )
22 21 imp 
 |-  ( ( y e. |^| G /\ s e. G ) -> y e. s )
23 22 adantll 
 |-  ( ( ( ph /\ y e. |^| G ) /\ s e. G ) -> y e. s )
24 saldifcl 
 |-  ( ( s e. SAlg /\ y e. s ) -> ( U. s \ y ) e. s )
25 20 23 24 syl2anc 
 |-  ( ( ( ph /\ y e. |^| G ) /\ s e. G ) -> ( U. s \ y ) e. s )
26 19 25 eqeltrd 
 |-  ( ( ( ph /\ y e. |^| G ) /\ s e. G ) -> ( U. |^| G \ y ) e. s )
27 26 ralrimiva 
 |-  ( ( ph /\ y e. |^| G ) -> A. s e. G ( U. |^| G \ y ) e. s )
28 intex 
 |-  ( G =/= (/) <-> |^| G e. _V )
29 28 biimpi 
 |-  ( G =/= (/) -> |^| G e. _V )
30 2 29 syl 
 |-  ( ph -> |^| G e. _V )
31 30 uniexd 
 |-  ( ph -> U. |^| G e. _V )
32 31 difexd 
 |-  ( ph -> ( U. |^| G \ y ) e. _V )
33 32 adantr 
 |-  ( ( ph /\ y e. |^| G ) -> ( U. |^| G \ y ) e. _V )
34 elintg 
 |-  ( ( U. |^| G \ y ) e. _V -> ( ( U. |^| G \ y ) e. |^| G <-> A. s e. G ( U. |^| G \ y ) e. s ) )
35 33 34 syl 
 |-  ( ( ph /\ y e. |^| G ) -> ( ( U. |^| G \ y ) e. |^| G <-> A. s e. G ( U. |^| G \ y ) e. s ) )
36 27 35 mpbird 
 |-  ( ( ph /\ y e. |^| G ) -> ( U. |^| G \ y ) e. |^| G )
37 36 ralrimiva 
 |-  ( ph -> A. y e. |^| G ( U. |^| G \ y ) e. |^| G )
38 5 ad4ant14 
 |-  ( ( ( ( ph /\ y e. ~P |^| G ) /\ y ~<_ _om ) /\ s e. G ) -> s e. SAlg )
39 elpwi 
 |-  ( y e. ~P |^| G -> y C_ |^| G )
40 39 adantr 
 |-  ( ( y e. ~P |^| G /\ s e. G ) -> y C_ |^| G )
41 intss1 
 |-  ( s e. G -> |^| G C_ s )
42 41 adantl 
 |-  ( ( y e. ~P |^| G /\ s e. G ) -> |^| G C_ s )
43 40 42 sstrd 
 |-  ( ( y e. ~P |^| G /\ s e. G ) -> y C_ s )
44 vex 
 |-  y e. _V
45 44 elpw 
 |-  ( y e. ~P s <-> y C_ s )
46 43 45 sylibr 
 |-  ( ( y e. ~P |^| G /\ s e. G ) -> y e. ~P s )
47 46 adantll 
 |-  ( ( ( ph /\ y e. ~P |^| G ) /\ s e. G ) -> y e. ~P s )
48 47 adantlr 
 |-  ( ( ( ( ph /\ y e. ~P |^| G ) /\ y ~<_ _om ) /\ s e. G ) -> y e. ~P s )
49 simplr 
 |-  ( ( ( ( ph /\ y e. ~P |^| G ) /\ y ~<_ _om ) /\ s e. G ) -> y ~<_ _om )
50 38 48 49 salunicl 
 |-  ( ( ( ( ph /\ y e. ~P |^| G ) /\ y ~<_ _om ) /\ s e. G ) -> U. y e. s )
51 50 ralrimiva 
 |-  ( ( ( ph /\ y e. ~P |^| G ) /\ y ~<_ _om ) -> A. s e. G U. y e. s )
52 vuniex 
 |-  U. y e. _V
53 52 a1i 
 |-  ( ( ( ph /\ y e. ~P |^| G ) /\ y ~<_ _om ) -> U. y e. _V )
54 elintg 
 |-  ( U. y e. _V -> ( U. y e. |^| G <-> A. s e. G U. y e. s ) )
55 53 54 syl 
 |-  ( ( ( ph /\ y e. ~P |^| G ) /\ y ~<_ _om ) -> ( U. y e. |^| G <-> A. s e. G U. y e. s ) )
56 51 55 mpbird 
 |-  ( ( ( ph /\ y e. ~P |^| G ) /\ y ~<_ _om ) -> U. y e. |^| G )
57 56 ex 
 |-  ( ( ph /\ y e. ~P |^| G ) -> ( y ~<_ _om -> U. y e. |^| G ) )
58 57 ralrimiva 
 |-  ( ph -> A. y e. ~P |^| G ( y ~<_ _om -> U. y e. |^| G ) )
59 13 37 58 3jca 
 |-  ( ph -> ( (/) e. |^| G /\ A. y e. |^| G ( U. |^| G \ y ) e. |^| G /\ A. y e. ~P |^| G ( y ~<_ _om -> U. y e. |^| G ) ) )
60 issal 
 |-  ( |^| G e. _V -> ( |^| G e. SAlg <-> ( (/) e. |^| G /\ A. y e. |^| G ( U. |^| G \ y ) e. |^| G /\ A. y e. ~P |^| G ( y ~<_ _om -> U. y e. |^| G ) ) ) )
61 30 60 syl 
 |-  ( ph -> ( |^| G e. SAlg <-> ( (/) e. |^| G /\ A. y e. |^| G ( U. |^| G \ y ) e. |^| G /\ A. y e. ~P |^| G ( y ~<_ _om -> U. y e. |^| G ) ) ) )
62 59 61 mpbird 
 |-  ( ph -> |^| G e. SAlg )