Theorem sssalgen

Description: A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypothesis	sssalgen.1	⊢ 𝑆 = ( SalGen ‘ 𝑋 )
Assertion	sssalgen	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		sssalgen.1	⊢ 𝑆 = ( SalGen ‘ 𝑋 )
2		ssint	⊢ ( 𝑋 ⊆ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ↔ ∀ 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } 𝑋 ⊆ 𝑡 )
3		unieq	⊢ ( 𝑠 = 𝑡 → ∪ 𝑠 = ∪ 𝑡 )
4	3	eqeq1d	⊢ ( 𝑠 = 𝑡 → ( ∪ 𝑠 = ∪ 𝑋 ↔ ∪ 𝑡 = ∪ 𝑋 ) )
5		sseq2	⊢ ( 𝑠 = 𝑡 → ( 𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝑡 ) )
6	4 5	anbi12d	⊢ ( 𝑠 = 𝑡 → ( ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) ↔ ( ∪ 𝑡 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑡 ) ) )
7	6	elrab	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ↔ ( 𝑡 ∈ SAlg ∧ ( ∪ 𝑡 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑡 ) ) )
8	7	biimpi	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → ( 𝑡 ∈ SAlg ∧ ( ∪ 𝑡 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑡 ) ) )
9	8	simprrd	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → 𝑋 ⊆ 𝑡 )
10	2 9	mprgbir	⊢ 𝑋 ⊆ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) }
11	10	a1i	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ⊆ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
12		salgenval	⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
13	1 12	syl5req	⊢ ( 𝑋 ∈ 𝑉 → ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } = 𝑆 )
14	11 13	sseqtrd	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝑆 )