Theorem salgencl

Description: SalGen actually generates a sigma-algebra. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Assertion	salgencl	⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) ∈ SAlg )

Proof

Step	Hyp	Ref	Expression
1		salgenval	⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
2		ssrab2	⊢ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ⊆ SAlg
3	2	a1i	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ⊆ SAlg )
4		salgenn0	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ≠ ∅ )
5		unieq	⊢ ( 𝑠 = 𝑡 → ∪ 𝑠 = ∪ 𝑡 )
6	5	eqeq1d	⊢ ( 𝑠 = 𝑡 → ( ∪ 𝑠 = ∪ 𝑋 ↔ ∪ 𝑡 = ∪ 𝑋 ) )
7		sseq2	⊢ ( 𝑠 = 𝑡 → ( 𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝑡 ) )
8	6 7	anbi12d	⊢ ( 𝑠 = 𝑡 → ( ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) ↔ ( ∪ 𝑡 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑡 ) ) )
9	8	elrab	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ↔ ( 𝑡 ∈ SAlg ∧ ( ∪ 𝑡 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑡 ) ) )
10	9	biimpi	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → ( 𝑡 ∈ SAlg ∧ ( ∪ 𝑡 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑡 ) ) )
11	10	simprld	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → ∪ 𝑡 = ∪ 𝑋 )
12	11	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ) → ∪ 𝑡 = ∪ 𝑋 )
13	3 4 12	intsal	⊢ ( 𝑋 ∈ 𝑉 → ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ∈ SAlg )
14	1 13	eqeltrd	⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) ∈ SAlg )