Theorem saliincl

Description: SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	saliincl.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	saliincl.kct	⊢ ( 𝜑 → 𝐾 ≼ ω )
	saliincl.kn0	⊢ ( 𝜑 → 𝐾 ≠ ∅ )
	saliincl.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
Assertion	saliincl	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		saliincl.s	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
2		saliincl.kct	⊢ ( 𝜑 → 𝐾 ≼ ω )
3		saliincl.kn0	⊢ ( 𝜑 → 𝐾 ≠ ∅ )
4		saliincl.e	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
5		elssuni	⊢ ( 𝐸 ∈ 𝑆 → 𝐸 ⊆ ∪ 𝑆 )
6	4 5	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ⊆ ∪ 𝑆 )
7		df-ss	⊢ ( 𝐸 ⊆ ∪ 𝑆 ↔ ( 𝐸 ∩ ∪ 𝑆 ) = 𝐸 )
8	6 7	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝐸 ∩ ∪ 𝑆 ) = 𝐸 )
9	8	eqcomd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 = ( 𝐸 ∩ ∪ 𝑆 ) )
10		incom	⊢ ( 𝐸 ∩ ∪ 𝑆 ) = ( ∪ 𝑆 ∩ 𝐸 )
11	10	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝐸 ∩ ∪ 𝑆 ) = ( ∪ 𝑆 ∩ 𝐸 ) )
12		dfin4	⊢ ( ∪ 𝑆 ∩ 𝐸 ) = ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) )
13	12	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( ∪ 𝑆 ∩ 𝐸 ) = ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) )
14	9 11 13	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 = ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) )
15	14	iineq2dv	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 = ∩ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) )
16		iindif2	⊢ ( 𝐾 ≠ ∅ → ∩ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) = ( ∪ 𝑆 ∖ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ) )
17	3 16	syl	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) = ( ∪ 𝑆 ∖ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ) )
18	15 17	eqtrd	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 = ( ∪ 𝑆 ∖ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ) )
19	1	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝑆 ∈ SAlg )
20		saldifcl	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 )
21	19 4 20	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 )
22	1 2 21	saliuncl	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 )
23		saldifcl	⊢ ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ) ∈ 𝑆 )
24	1 22 23	syl2anc	⊢ ( 𝜑 → ( ∪ 𝑆 ∖ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ) ∈ 𝑆 )
25	18 24	eqeltrd	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )