Theorem salgenval

Description: The sigma-algebra generated by a set. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Assertion	salgenval	⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )

Proof

Step	Hyp	Ref	Expression
1		df-salgen	⊢ SalGen = ( 𝑥 ∈ V ↦ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 ) } )
2	1	a1i	⊢ ( 𝑋 ∈ 𝑉 → SalGen = ( 𝑥 ∈ V ↦ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 ) } ) )
3		unieq	⊢ ( 𝑥 = 𝑋 → ∪ 𝑥 = ∪ 𝑋 )
4	3	eqeq2d	⊢ ( 𝑥 = 𝑋 → ( ∪ 𝑠 = ∪ 𝑥 ↔ ∪ 𝑠 = ∪ 𝑋 ) )
5		sseq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝑠 ) )
6	4 5	anbi12d	⊢ ( 𝑥 = 𝑋 → ( ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 ) ↔ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) ) )
7	6	rabbidv	⊢ ( 𝑥 = 𝑋 → { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 ) } = { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
8	7	inteqd	⊢ ( 𝑥 = 𝑋 → ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 ) } = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
9	8	adantl	⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑥 = 𝑋 ) → ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑥 ∧ 𝑥 ⊆ 𝑠 ) } = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
10		elex	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ V )
11		uniexg	⊢ ( 𝑋 ∈ 𝑉 → ∪ 𝑋 ∈ V )
12		pwsal	⊢ ( ∪ 𝑋 ∈ V → 𝒫 ∪ 𝑋 ∈ SAlg )
13	11 12	syl	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 ∪ 𝑋 ∈ SAlg )
14		unipw	⊢ ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋
15	14	a1i	⊢ ( 𝑋 ∈ 𝑉 → ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 )
16		pwuni	⊢ 𝑋 ⊆ 𝒫 ∪ 𝑋
17	16	a1i	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝒫 ∪ 𝑋 )
18	13 15 17	jca32	⊢ ( 𝑋 ∈ 𝑉 → ( 𝒫 ∪ 𝑋 ∈ SAlg ∧ ( ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝒫 ∪ 𝑋 ) ) )
19		unieq	⊢ ( 𝑠 = 𝒫 ∪ 𝑋 → ∪ 𝑠 = ∪ 𝒫 ∪ 𝑋 )
20	19	eqeq1d	⊢ ( 𝑠 = 𝒫 ∪ 𝑋 → ( ∪ 𝑠 = ∪ 𝑋 ↔ ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 ) )
21		sseq2	⊢ ( 𝑠 = 𝒫 ∪ 𝑋 → ( 𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝒫 ∪ 𝑋 ) )
22	20 21	anbi12d	⊢ ( 𝑠 = 𝒫 ∪ 𝑋 → ( ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) ↔ ( ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝒫 ∪ 𝑋 ) ) )
23	22	elrab	⊢ ( 𝒫 ∪ 𝑋 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ↔ ( 𝒫 ∪ 𝑋 ∈ SAlg ∧ ( ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝒫 ∪ 𝑋 ) ) )
24	18 23	sylibr	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 ∪ 𝑋 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
25	24	ne0d	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ≠ ∅ )
26		intex	⊢ ( { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ≠ ∅ ↔ ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ∈ V )
27	25 26	sylib	⊢ ( 𝑋 ∈ 𝑉 → ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ∈ V )
28	2 9 10 27	fvmptd	⊢ ( 𝑋 ∈ 𝑉 → ( SalGen ‘ 𝑋 ) = ∩ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )