Theorem sigagenss2

Description: Sufficient condition for inclusion of sigma-algebras. This is used to prove equality of sigma-algebras. (Contributed by Thierry Arnoux, 10-Oct-2017)

	Ref	Expression
Assertion	sigagenss2	$$⊢\left(\bigcup A=\bigcup B\wedge A\subseteq 𝛔\left(B\right)\wedge B\in V\right)\to 𝛔\left(A\right)\subseteq 𝛔\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		sigagensiga	$$⊢B\in V\to 𝛔\left(B\right)\in \mathrm{sigAlgebra}\left(\bigcup B\right)$$
2	1	3ad2ant3	$$⊢\left(\bigcup A=\bigcup B\wedge A\subseteq 𝛔\left(B\right)\wedge B\in V\right)\to 𝛔\left(B\right)\in \mathrm{sigAlgebra}\left(\bigcup B\right)$$
3		simp1	$$⊢\left(\bigcup A=\bigcup B\wedge A\subseteq 𝛔\left(B\right)\wedge B\in V\right)\to \bigcup A=\bigcup B$$
4	3	fveq2d	$$⊢\left(\bigcup A=\bigcup B\wedge A\subseteq 𝛔\left(B\right)\wedge B\in V\right)\to \mathrm{sigAlgebra}\left(\bigcup A\right)=\mathrm{sigAlgebra}\left(\bigcup B\right)$$
5	2 4	eleqtrrd	$$⊢\left(\bigcup A=\bigcup B\wedge A\subseteq 𝛔\left(B\right)\wedge B\in V\right)\to 𝛔\left(B\right)\in \mathrm{sigAlgebra}\left(\bigcup A\right)$$
6		simp2	$$⊢\left(\bigcup A=\bigcup B\wedge A\subseteq 𝛔\left(B\right)\wedge B\in V\right)\to A\subseteq 𝛔\left(B\right)$$
7		sigagenss	$$⊢\left(𝛔\left(B\right)\in \mathrm{sigAlgebra}\left(\bigcup A\right)\wedge A\subseteq 𝛔\left(B\right)\right)\to 𝛔\left(A\right)\subseteq 𝛔\left(B\right)$$
8	5 6 7	syl2anc	$$⊢\left(\bigcup A=\bigcup B\wedge A\subseteq 𝛔\left(B\right)\wedge B\in V\right)\to 𝛔\left(A\right)\subseteq 𝛔\left(B\right)$$