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	⊢ ( 𝜑 → 𝐺 ⊆ SAlg )
	intsaluni.gn0	⊢ ( 𝜑 → 𝐺 ≠ ∅ )
	intsaluni.x	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∪ 𝑠 = 𝑋 )
Assertion	intsaluni	⊢ ( 𝜑 → ∪ ∩ 𝐺 = 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		intsaluni.ga	⊢ ( 𝜑 → 𝐺 ⊆ SAlg )
2		intsaluni.gn0	⊢ ( 𝜑 → 𝐺 ≠ ∅ )
3		intsaluni.x	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∪ 𝑠 = 𝑋 )
4		nfv	⊢ Ⅎ 𝑠 𝜑
5		nfv	⊢ Ⅎ 𝑠 ∪ ∩ 𝐺 = 𝑋
6		n0	⊢ ( 𝐺 ≠ ∅ ↔ ∃ 𝑠 𝑠 ∈ 𝐺 )
7	6	biimpi	⊢ ( 𝐺 ≠ ∅ → ∃ 𝑠 𝑠 ∈ 𝐺 )
8	2 7	syl	⊢ ( 𝜑 → ∃ 𝑠 𝑠 ∈ 𝐺 )
9		intss1	⊢ ( 𝑠 ∈ 𝐺 → ∩ 𝐺 ⊆ 𝑠 )
10	9	unissd	⊢ ( 𝑠 ∈ 𝐺 → ∪ ∩ 𝐺 ⊆ ∪ 𝑠 )
11	10	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∪ ∩ 𝐺 ⊆ ∪ 𝑠 )
12	11 3	sseqtrd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∪ ∩ 𝐺 ⊆ 𝑋 )
13	3	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ∧ 𝑡 ∈ 𝐺 ) → ∪ 𝑠 = 𝑋 )
14		eleq1w	⊢ ( 𝑠 = 𝑡 → ( 𝑠 ∈ 𝐺 ↔ 𝑡 ∈ 𝐺 ) )
15	14	anbi2d	⊢ ( 𝑠 = 𝑡 → ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ↔ ( 𝜑 ∧ 𝑡 ∈ 𝐺 ) ) )
16		unieq	⊢ ( 𝑠 = 𝑡 → ∪ 𝑠 = ∪ 𝑡 )
17	16	eqeq1d	⊢ ( 𝑠 = 𝑡 → ( ∪ 𝑠 = 𝑋 ↔ ∪ 𝑡 = 𝑋 ) )
18	15 17	imbi12d	⊢ ( 𝑠 = 𝑡 → ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∪ 𝑠 = 𝑋 ) ↔ ( ( 𝜑 ∧ 𝑡 ∈ 𝐺 ) → ∪ 𝑡 = 𝑋 ) ) )
19	18 3	chvarvv	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐺 ) → ∪ 𝑡 = 𝑋 )
20	19	eqcomd	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐺 ) → 𝑋 = ∪ 𝑡 )
21	20	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ∧ 𝑡 ∈ 𝐺 ) → 𝑋 = ∪ 𝑡 )
22	13 21	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ∧ 𝑡 ∈ 𝐺 ) → ∪ 𝑠 = ∪ 𝑡 )
23	1	sselda	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐺 ) → 𝑡 ∈ SAlg )
24		saluni	⊢ ( 𝑡 ∈ SAlg → ∪ 𝑡 ∈ 𝑡 )
25	23 24	syl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐺 ) → ∪ 𝑡 ∈ 𝑡 )
26	25	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ∧ 𝑡 ∈ 𝐺 ) → ∪ 𝑡 ∈ 𝑡 )
27	22 26	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ∧ 𝑡 ∈ 𝐺 ) → ∪ 𝑠 ∈ 𝑡 )
28	27	ralrimiva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∀ 𝑡 ∈ 𝐺 ∪ 𝑠 ∈ 𝑡 )
29		uniexg	⊢ ( 𝑠 ∈ 𝐺 → ∪ 𝑠 ∈ V )
30	29	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∪ 𝑠 ∈ V )
31		elintg	⊢ ( ∪ 𝑠 ∈ V → ( ∪ 𝑠 ∈ ∩ 𝐺 ↔ ∀ 𝑡 ∈ 𝐺 ∪ 𝑠 ∈ 𝑡 ) )
32	30 31	syl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ( ∪ 𝑠 ∈ ∩ 𝐺 ↔ ∀ 𝑡 ∈ 𝐺 ∪ 𝑠 ∈ 𝑡 ) )
33	28 32	mpbird	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∪ 𝑠 ∈ ∩ 𝐺 )
34	33	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → ∪ 𝑠 ∈ ∩ 𝐺 )
35		simpr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
36	3	eqcomd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → 𝑋 = ∪ 𝑠 )
37	36	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑋 = ∪ 𝑠 )
38	35 37	eleqtrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ∪ 𝑠 )
39		eleq2	⊢ ( 𝑦 = ∪ 𝑠 → ( 𝑥 ∈ 𝑦 ↔ 𝑥 ∈ ∪ 𝑠 ) )
40	39	rspcev	⊢ ( ( ∪ 𝑠 ∈ ∩ 𝐺 ∧ 𝑥 ∈ ∪ 𝑠 ) → ∃ 𝑦 ∈ ∩ 𝐺 𝑥 ∈ 𝑦 )
41	34 38 40	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → ∃ 𝑦 ∈ ∩ 𝐺 𝑥 ∈ 𝑦 )
42		eluni2	⊢ ( 𝑥 ∈ ∪ ∩ 𝐺 ↔ ∃ 𝑦 ∈ ∩ 𝐺 𝑥 ∈ 𝑦 )
43	41 42	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ ∪ ∩ 𝐺 )
44	12 43	eqelssd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝐺 ) → ∪ ∩ 𝐺 = 𝑋 )
45	44	ex	⊢ ( 𝜑 → ( 𝑠 ∈ 𝐺 → ∪ ∩ 𝐺 = 𝑋 ) )
46	4 5 8 45	exlimimdd	⊢ ( 𝜑 → ∪ ∩ 𝐺 = 𝑋 )