Theorem saliinclf

Description: SAlg sigma-algebra is closed under countable indexed intersection. (Contributed by Glauco Siliprandi, 24-Jan-2025)

	Ref	Expression
Hypotheses	saliinclf.1	⊢ Ⅎ 𝑘 𝜑
	saliinclf.2	⊢ Ⅎ 𝑘 𝑆
	saliinclf.3	⊢ Ⅎ 𝑘 𝐾
	saliinclf.4	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
	saliinclf.5	⊢ ( 𝜑 → 𝐾 ≼ ω )
	saliinclf.6	⊢ ( 𝜑 → 𝐾 ≠ ∅ )
	saliinclf.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
Assertion	saliinclf	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		saliinclf.1	⊢ Ⅎ 𝑘 𝜑
2		saliinclf.2	⊢ Ⅎ 𝑘 𝑆
3		saliinclf.3	⊢ Ⅎ 𝑘 𝐾
4		saliinclf.4	⊢ ( 𝜑 → 𝑆 ∈ SAlg )
5		saliinclf.5	⊢ ( 𝜑 → 𝐾 ≼ ω )
6		saliinclf.6	⊢ ( 𝜑 → 𝐾 ≠ ∅ )
7		saliinclf.7	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ∈ 𝑆 )
8		incom	⊢ ( 𝐸 ∩ ∪ 𝑆 ) = ( ∪ 𝑆 ∩ 𝐸 )
9		elssuni	⊢ ( 𝐸 ∈ 𝑆 → 𝐸 ⊆ ∪ 𝑆 )
10	7 9	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 ⊆ ∪ 𝑆 )
11		dfss2	⊢ ( 𝐸 ⊆ ∪ 𝑆 ↔ ( 𝐸 ∩ ∪ 𝑆 ) = 𝐸 )
12	10 11	sylib	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( 𝐸 ∩ ∪ 𝑆 ) = 𝐸 )
13		dfin4	⊢ ( ∪ 𝑆 ∩ 𝐸 ) = ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) )
14	13	a1i	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( ∪ 𝑆 ∩ 𝐸 ) = ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) )
15	8 12 14	3eqtr3a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → 𝐸 = ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) )
16	1 15	iineq2d	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 = ∩ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) )
17	2	nfuni	⊢ Ⅎ 𝑘 ∪ 𝑆
18	3 17	iindif2f	⊢ ( 𝐾 ≠ ∅ → ∩ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) = ( ∪ 𝑆 ∖ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ) )
19	6 18	syl	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ ( ∪ 𝑆 ∖ 𝐸 ) ) = ( ∪ 𝑆 ∖ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ) )
20	16 19	eqtrd	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 = ( ∪ 𝑆 ∖ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ) )
21		saldifcl	⊢ ( ( 𝑆 ∈ SAlg ∧ 𝐸 ∈ 𝑆 ) → ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 )
22	4 7 21	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝐾 ) → ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 )
23	1 2 3 4 5 22	saliunclf	⊢ ( 𝜑 → ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 )
24		saldifcl	⊢ ( ( 𝑆 ∈ SAlg ∧ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ∈ 𝑆 ) → ( ∪ 𝑆 ∖ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ) ∈ 𝑆 )
25	4 23 24	syl2anc	⊢ ( 𝜑 → ( ∪ 𝑆 ∖ ∪ 𝑘 ∈ 𝐾 ( ∪ 𝑆 ∖ 𝐸 ) ) ∈ 𝑆 )
26	20 25	eqeltrd	⊢ ( 𝜑 → ∩ 𝑘 ∈ 𝐾 𝐸 ∈ 𝑆 )