Theorem salgenuni

Description: The base set of the sigma-algebra generated by a set is the union of the set itself. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Hypotheses	salgenuni.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	salgenuni.s	⊢ 𝑆 = ( SalGen ‘ 𝑋 )
	salgenuni.u	⊢ 𝑈 = ∪ 𝑋
Assertion	salgenuni	⊢ ( 𝜑 → ∪ 𝑆 = 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		salgenuni.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		salgenuni.s	⊢ 𝑆 = ( SalGen ‘ 𝑋 )
3		salgenuni.u	⊢ 𝑈 = ∪ 𝑋
4	2	a1i	⊢ ( 𝜑 → 𝑆 = ( SalGen ‘ 𝑋 ) )
5		salgenval	⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
6	1 5	syl	⊢ ( 𝜑 → ( SalGen ‘ 𝑋 ) = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
7	4 6	eqtrd	⊢ ( 𝜑 → 𝑆 = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
8	7	unieqd	⊢ ( 𝜑 → ∪ 𝑆 = ∪ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
9		ssrab2	⊢ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ⊆ SAlg
10	9	a1i	⊢ ( 𝜑 → { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ⊆ SAlg )
11		salgenn0	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ≠ ∅ )
12	1 11	syl	⊢ ( 𝜑 → { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ≠ ∅ )
13		unieq	⊢ ( 𝑠 = 𝑡 → ∪ 𝑠 = ∪ 𝑡 )
14	13	eqeq1d	⊢ ( 𝑠 = 𝑡 → ( ∪ 𝑠 = ∪ 𝑋 ↔ ∪ 𝑡 = ∪ 𝑋 ) )
15		sseq2	⊢ ( 𝑠 = 𝑡 → ( 𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝑡 ) )
16	14 15	anbi12d	⊢ ( 𝑠 = 𝑡 → ( ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) ↔ ( ∪ 𝑡 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑡 ) ) )
17	16	elrab	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ↔ ( 𝑡 ∈ SAlg ∧ ( ∪ 𝑡 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑡 ) ) )
18	17	biimpi	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → ( 𝑡 ∈ SAlg ∧ ( ∪ 𝑡 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑡 ) ) )
19	18	simprld	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → ∪ 𝑡 = ∪ 𝑋 )
20	3	eqcomi	⊢ ∪ 𝑋 = 𝑈
21	20	a1i	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → ∪ 𝑋 = 𝑈 )
22	19 21	eqtrd	⊢ ( 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } → ∪ 𝑡 = 𝑈 )
23	22	adantl	⊢ ( ( 𝜑 ∧ 𝑡 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ) → ∪ 𝑡 = 𝑈 )
24	10 12 23	intsaluni	⊢ ( 𝜑 → ∪ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } = 𝑈 )
25	8 24	eqtrd	⊢ ( 𝜑 → ∪ 𝑆 = 𝑈 )