salgencl

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

		Ref	Expression
	Assertion	salgencl	$⊢ X \in V \to SalGen (X) \in SAlg$

Step	Hyp	Ref	Expression
1		salgenval	$⊢ X \in V \to SalGen (X) = ⋂ \{s \in SAlg \| (⋃ s = ⋃ X \land X \subseteq s)\}$
2		ssrab2	$⊢ \{s \in SAlg \| (⋃ s = ⋃ X \land X \subseteq s)\} \subseteq SAlg$
3	2	a1i	$⊢ X \in V \to \{s \in SAlg \| (⋃ s = ⋃ X \land X \subseteq s)\} \subseteq SAlg$
4		salgenn0	$⊢ X \in V \to \{s \in SAlg \| (⋃ s = ⋃ X \land X \subseteq s)\} \neq \emptyset$
5		unieq	$⊢ s = t \to ⋃ s = ⋃ t$
6	5	eqeq1d	$⊢ s = t \to (⋃ s = ⋃ X \leftrightarrow ⋃ t = ⋃ X)$
7		sseq2	$⊢ s = t \to (X \subseteq s \leftrightarrow X \subseteq t)$
8	6 7	anbi12d	$⊢ s = t \to ((⋃ s = ⋃ X \land X \subseteq s) \leftrightarrow (⋃ t = ⋃ X \land X \subseteq t))$
9	8	elrab	$⊢ t \in \{s \in SAlg \| (⋃ s = ⋃ X \land X \subseteq s)\} \leftrightarrow (t \in SAlg \land (⋃ t = ⋃ X \land X \subseteq t))$
10	9	biimpi	$⊢ t \in \{s \in SAlg \| (⋃ s = ⋃ X \land X \subseteq s)\} \to (t \in SAlg \land (⋃ t = ⋃ X \land X \subseteq t))$
11	10	simprld	$⊢ t \in \{s \in SAlg \| (⋃ s = ⋃ X \land X \subseteq s)\} \to ⋃ t = ⋃ X$
12	11	adantl	$⊢ (X \in V \land t \in \{s \in SAlg \| (⋃ s = ⋃ X \land X \subseteq s)\}) \to ⋃ t = ⋃ X$
13	3 4 12	intsal	$⊢ X \in V \to ⋂ \{s \in SAlg \| (⋃ s = ⋃ X \land X \subseteq s)\} \in SAlg$
14	1 13	eqeltrd	$⊢ X \in V \to SalGen (X) \in SAlg$

Metamath Proof Explorer