Theorem unisalgen2

Description: The union of a set belongs is equal to the union of the sigma-algebra generated by the set. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	unisalgen2.x	$$⊢\phi \to A\in V$$
	unisalgen2.s	$$⊢S=\mathrm{SalGen}\left(A\right)$$
Assertion	unisalgen2	$$⊢\phi \to \bigcup S=\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		unisalgen2.x	$$⊢\phi \to A\in V$$
2		unisalgen2.s	$$⊢S=\mathrm{SalGen}\left(A\right)$$
3	2	eqcomi	$$⊢\mathrm{SalGen}\left(A\right)=S$$
4	3	a1i	$$⊢\phi \to \mathrm{SalGen}\left(A\right)=S$$
5	1	dfsalgen2	$$⊢\phi \to \left(\mathrm{SalGen}\left(A\right)=S\leftrightarrow \left(\left(S\in \mathrm{SAlg}\wedge \bigcup S=\bigcup A\wedge A\subseteq S\right)\wedge \forall x\in \mathrm{SAlg}\left(\left(\bigcup x=\bigcup A\wedge A\subseteq x\right)\to S\subseteq x\right)\right)\right)$$
6	4 5	mpbid	$$⊢\phi \to \left(\left(S\in \mathrm{SAlg}\wedge \bigcup S=\bigcup A\wedge A\subseteq S\right)\wedge \forall x\in \mathrm{SAlg}\left(\left(\bigcup x=\bigcup A\wedge A\subseteq x\right)\to S\subseteq x\right)\right)$$
7	6	simpld	$$⊢\phi \to \left(S\in \mathrm{SAlg}\wedge \bigcup S=\bigcup A\wedge A\subseteq S\right)$$
8	7	simp2d	$$⊢\phi \to \bigcup S=\bigcup A$$