Theorem salgenn0

Description: The set used in the definition of the generated sigma-algebra, is not empty. (Contributed by Glauco Siliprandi, 3-Jan-2021)

	Ref	Expression
Assertion	salgenn0	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		uniexg	⊢ ( 𝑋 ∈ 𝑉 → ∪ 𝑋 ∈ V )
2		pwsal	⊢ ( ∪ 𝑋 ∈ V → 𝒫 ∪ 𝑋 ∈ SAlg )
3	1 2	syl	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 ∪ 𝑋 ∈ SAlg )
4		unipw	⊢ ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋
5	4	a1i	⊢ ( 𝑋 ∈ 𝑉 → ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 )
6		pwuni	⊢ 𝑋 ⊆ 𝒫 ∪ 𝑋
7	6	a1i	⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ⊆ 𝒫 ∪ 𝑋 )
8	5 7	jca	⊢ ( 𝑋 ∈ 𝑉 → ( ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝒫 ∪ 𝑋 ) )
9	3 8	jca	⊢ ( 𝑋 ∈ 𝑉 → ( 𝒫 ∪ 𝑋 ∈ SAlg ∧ ( ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝒫 ∪ 𝑋 ) ) )
10		unieq	⊢ ( 𝑠 = 𝒫 ∪ 𝑋 → ∪ 𝑠 = ∪ 𝒫 ∪ 𝑋 )
11	10	eqeq1d	⊢ ( 𝑠 = 𝒫 ∪ 𝑋 → ( ∪ 𝑠 = ∪ 𝑋 ↔ ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 ) )
12		sseq2	⊢ ( 𝑠 = 𝒫 ∪ 𝑋 → ( 𝑋 ⊆ 𝑠 ↔ 𝑋 ⊆ 𝒫 ∪ 𝑋 ) )
13	11 12	anbi12d	⊢ ( 𝑠 = 𝒫 ∪ 𝑋 → ( ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) ↔ ( ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝒫 ∪ 𝑋 ) ) )
14	13	elrab	⊢ ( 𝒫 ∪ 𝑋 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ↔ ( 𝒫 ∪ 𝑋 ∈ SAlg ∧ ( ∪ 𝒫 ∪ 𝑋 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝒫 ∪ 𝑋 ) ) )
15	9 14	sylibr	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 ∪ 𝑋 ∈ { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } )
16	15	ne0d	⊢ ( 𝑋 ∈ 𝑉 → { 𝑠 ∈ SAlg ∣ ( ∪ 𝑠 = ∪ 𝑋 ∧ 𝑋 ⊆ 𝑠 ) } ≠ ∅ )