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 φ G SAlg
intsaluni.gn0 φ G
intsaluni.x φ s G s = X
Assertion intsaluni φ G = X

Proof

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