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	$$⊢\phi \to G\subseteq \mathrm{SAlg}$$
	intsaluni.gn0	$$⊢\phi \to G\ne \varnothing$$
	intsaluni.x	$$⊢\left(\phi \wedge s\in G\right)\to \bigcup s=X$$
Assertion	intsaluni	$$⊢\phi \to \bigcup \bigcap G=X$$

Proof

Step	Hyp	Ref	Expression
1		intsaluni.ga	$$⊢\phi \to G\subseteq \mathrm{SAlg}$$
2		intsaluni.gn0	$$⊢\phi \to G\ne \varnothing$$
3		intsaluni.x	$$⊢\left(\phi \wedge s\in G\right)\to \bigcup s=X$$
4		nfv	$$⊢Ⅎs\phi$$
5		nfv	$$⊢Ⅎs\bigcup \bigcap G=X$$
6		n0	$$⊢G\ne \varnothing \leftrightarrow \exists ss\in G$$
7	6	biimpi	$$⊢G\ne \varnothing \to \exists ss\in G$$
8	2 7	syl	$$⊢\phi \to \exists ss\in G$$
9		intss1	$$⊢s\in G\to \bigcap G\subseteq s$$
10	9	unissd	$$⊢s\in G\to \bigcup \bigcap G\subseteq \bigcup s$$
11	10	adantl	$$⊢\left(\phi \wedge s\in G\right)\to \bigcup \bigcap G\subseteq \bigcup s$$
12	11 3	sseqtrd	$$⊢\left(\phi \wedge s\in G\right)\to \bigcup \bigcap G\subseteq X$$
13	3	adantr	$$⊢\left(\left(\phi \wedge s\in G\right)\wedge t\in G\right)\to \bigcup s=X$$
14		eleq1w	$$⊢s=t\to \left(s\in G\leftrightarrow t\in G\right)$$
15	14	anbi2d	$$⊢s=t\to \left(\left(\phi \wedge s\in G\right)\leftrightarrow \left(\phi \wedge t\in G\right)\right)$$
16		unieq	$$⊢s=t\to \bigcup s=\bigcup t$$
17	16	eqeq1d	$$⊢s=t\to \left(\bigcup s=X\leftrightarrow \bigcup t=X\right)$$
18	15 17	imbi12d	$$⊢s=t\to \left(\left(\left(\phi \wedge s\in G\right)\to \bigcup s=X\right)\leftrightarrow \left(\left(\phi \wedge t\in G\right)\to \bigcup t=X\right)\right)$$
19	18 3	chvarvv	$$⊢\left(\phi \wedge t\in G\right)\to \bigcup t=X$$
20	19	eqcomd	$$⊢\left(\phi \wedge t\in G\right)\to X=\bigcup t$$
21	20	adantlr	$$⊢\left(\left(\phi \wedge s\in G\right)\wedge t\in G\right)\to X=\bigcup t$$
22	13 21	eqtrd	$$⊢\left(\left(\phi \wedge s\in G\right)\wedge t\in G\right)\to \bigcup s=\bigcup t$$
23	1	sselda	$$⊢\left(\phi \wedge t\in G\right)\to t\in \mathrm{SAlg}$$
24		saluni	$$⊢t\in \mathrm{SAlg}\to \bigcup t\in t$$
25	23 24	syl	$$⊢\left(\phi \wedge t\in G\right)\to \bigcup t\in t$$
26	25	adantlr	$$⊢\left(\left(\phi \wedge s\in G\right)\wedge t\in G\right)\to \bigcup t\in t$$
27	22 26	eqeltrd	$$⊢\left(\left(\phi \wedge s\in G\right)\wedge t\in G\right)\to \bigcup s\in t$$
28	27	ralrimiva	$$⊢\left(\phi \wedge s\in G\right)\to \forall t\in G\bigcup s\in t$$
29		uniexg	$$⊢s\in G\to \bigcup s\in \mathrm{V}$$
30	29	adantl	$$⊢\left(\phi \wedge s\in G\right)\to \bigcup s\in \mathrm{V}$$
31		elintg	$$⊢\bigcup s\in \mathrm{V}\to \left(\bigcup s\in \bigcap G\leftrightarrow \forall t\in G\bigcup s\in t\right)$$
32	30 31	syl	$$⊢\left(\phi \wedge s\in G\right)\to \left(\bigcup s\in \bigcap G\leftrightarrow \forall t\in G\bigcup s\in t\right)$$
33	28 32	mpbird	$$⊢\left(\phi \wedge s\in G\right)\to \bigcup s\in \bigcap G$$
34	33	adantr	$$⊢\left(\left(\phi \wedge s\in G\right)\wedge x\in X\right)\to \bigcup s\in \bigcap G$$
35		simpr	$$⊢\left(\left(\phi \wedge s\in G\right)\wedge x\in X\right)\to x\in X$$
36	3	eqcomd	$$⊢\left(\phi \wedge s\in G\right)\to X=\bigcup s$$
37	36	adantr	$$⊢\left(\left(\phi \wedge s\in G\right)\wedge x\in X\right)\to X=\bigcup s$$
38	35 37	eleqtrd	$$⊢\left(\left(\phi \wedge s\in G\right)\wedge x\in X\right)\to x\in \bigcup s$$
39		eleq2	$$⊢y=\bigcup s\to \left(x\in y\leftrightarrow x\in \bigcup s\right)$$
40	39	rspcev	$$⊢\left(\bigcup s\in \bigcap G\wedge x\in \bigcup s\right)\to \exists y\in \bigcap Gx\in y$$
41	34 38 40	syl2anc	$$⊢\left(\left(\phi \wedge s\in G\right)\wedge x\in X\right)\to \exists y\in \bigcap Gx\in y$$
42		eluni2	$$⊢x\in \bigcup \bigcap G\leftrightarrow \exists y\in \bigcap Gx\in y$$
43	41 42	sylibr	$$⊢\left(\left(\phi \wedge s\in G\right)\wedge x\in X\right)\to x\in \bigcup \bigcap G$$
44	12 43	eqelssd	$$⊢\left(\phi \wedge s\in G\right)\to \bigcup \bigcap G=X$$
45	44	ex	$$⊢\phi \to \left(s\in G\to \bigcup \bigcap G=X\right)$$
46	4 5 8 45	exlimimdd	$$⊢\phi \to \bigcup \bigcap G=X$$