Metamath Proof Explorer

Theorem intsaluni

Description: The union of an arbitrary intersection of sigma-algebras on the same set X , is X . (Contributed by Glauco Siliprandi, 17-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 intsaluni.ga 
 |-  ( ph -> G C_ SAlg )
2 intsaluni.gn0 
 |-  ( ph -> G =/= (/) )
3 intsaluni.x 
 |-  ( ( ph /\ s e. G ) -> U. s = X )
4 nfv 
 |-  F/ s ph
5 nfv 
 |-  F/ s U. |^| G = X
6 n0 
 |-  ( G =/= (/) <-> E. s s e. G )
7 6 biimpi 
 |-  ( G =/= (/) -> E. s s e. G )
8 2 7 syl 
 |-  ( ph -> E. s s e. G )
9 intss1 
 |-  ( s e. G -> |^| G C_ s )
10 9 unissd 
 |-  ( s e. G -> U. |^| G C_ U. s )
11 10 adantl 
 |-  ( ( ph /\ s e. G ) -> U. |^| G C_ U. s )
12 11 3 sseqtrd 
 |-  ( ( ph /\ s e. G ) -> U. |^| G C_ X )
13 3 adantr 
 |-  ( ( ( ph /\ s e. G ) /\ t e. G ) -> U. s = X )
14 eleq1w 
 |-  ( s = t -> ( s e. G <-> t e. G ) )
15 14 anbi2d 
 |-  ( s = t -> ( ( ph /\ s e. G ) <-> ( ph /\ t e. G ) ) )
16 unieq 
 |-  ( s = t -> U. s = U. t )
17 16 eqeq1d 
 |-  ( s = t -> ( U. s = X <-> U. t = X ) )
18 15 17 imbi12d 
 |-  ( s = t -> ( ( ( ph /\ s e. G ) -> U. s = X ) <-> ( ( ph /\ t e. G ) -> U. t = X ) ) )
19 18 3 chvarvv 
 |-  ( ( ph /\ t e. G ) -> U. t = X )
20 19 eqcomd 
 |-  ( ( ph /\ t e. G ) -> X = U. t )
21 20 adantlr 
 |-  ( ( ( ph /\ s e. G ) /\ t e. G ) -> X = U. t )
22 13 21 eqtrd 
 |-  ( ( ( ph /\ s e. G ) /\ t e. G ) -> U. s = U. t )
23 1 sselda 
 |-  ( ( ph /\ t e. G ) -> t e. SAlg )
24 saluni 
 |-  ( t e. SAlg -> U. t e. t )
25 23 24 syl 
 |-  ( ( ph /\ t e. G ) -> U. t e. t )
26 25 adantlr 
 |-  ( ( ( ph /\ s e. G ) /\ t e. G ) -> U. t e. t )
27 22 26 eqeltrd 
 |-  ( ( ( ph /\ s e. G ) /\ t e. G ) -> U. s e. t )
28 27 ralrimiva 
 |-  ( ( ph /\ s e. G ) -> A. t e. G U. s e. t )
29 uniexg 
 |-  ( s e. G -> U. s e. _V )
30 29 adantl 
 |-  ( ( ph /\ s e. G ) -> U. s e. _V )
31 elintg 
 |-  ( U. s e. _V -> ( U. s e. |^| G <-> A. t e. G U. s e. t ) )
32 30 31 syl 
 |-  ( ( ph /\ s e. G ) -> ( U. s e. |^| G <-> A. t e. G U. s e. t ) )
33 28 32 mpbird 
 |-  ( ( ph /\ s e. G ) -> U. s e. |^| G )
34 33 adantr 
 |-  ( ( ( ph /\ s e. G ) /\ x e. X ) -> U. s e. |^| G )
35 simpr 
 |-  ( ( ( ph /\ s e. G ) /\ x e. X ) -> x e. X )
36 3 eqcomd 
 |-  ( ( ph /\ s e. G ) -> X = U. s )
37 36 adantr 
 |-  ( ( ( ph /\ s e. G ) /\ x e. X ) -> X = U. s )
38 35 37 eleqtrd 
 |-  ( ( ( ph /\ s e. G ) /\ x e. X ) -> x e. U. s )
39 eleq2 
 |-  ( y = U. s -> ( x e. y <-> x e. U. s ) )
40 39 rspcev 
 |-  ( ( U. s e. |^| G /\ x e. U. s ) -> E. y e. |^| G x e. y )
41 34 38 40 syl2anc 
 |-  ( ( ( ph /\ s e. G ) /\ x e. X ) -> E. y e. |^| G x e. y )
42 eluni2 
 |-  ( x e. U. |^| G <-> E. y e. |^| G x e. y )
43 41 42 sylibr 
 |-  ( ( ( ph /\ s e. G ) /\ x e. X ) -> x e. U. |^| G )
44 12 43 eqelssd 
 |-  ( ( ph /\ s e. G ) -> U. |^| G = X )
45 44 ex 
 |-  ( ph -> ( s e. G -> U. |^| G = X ) )
46 4 5 8 45 exlimimdd 
 |-  ( ph -> U. |^| G = X )