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	⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ 𝐴 ⊆ ( sigaGen ‘ 𝐵 ) ∧ 𝐵 ∈ 𝑉 ) → ( sigaGen ‘ 𝐴 ) ⊆ ( sigaGen ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		sigagensiga	⊢ ( 𝐵 ∈ 𝑉 → ( sigaGen ‘ 𝐵 ) ∈ ( sigAlgebra ‘ ∪ 𝐵 ) )
2	1	3ad2ant3	⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ 𝐴 ⊆ ( sigaGen ‘ 𝐵 ) ∧ 𝐵 ∈ 𝑉 ) → ( sigaGen ‘ 𝐵 ) ∈ ( sigAlgebra ‘ ∪ 𝐵 ) )
3		simp1	⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ 𝐴 ⊆ ( sigaGen ‘ 𝐵 ) ∧ 𝐵 ∈ 𝑉 ) → ∪ 𝐴 = ∪ 𝐵 )
4	3	fveq2d	⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ 𝐴 ⊆ ( sigaGen ‘ 𝐵 ) ∧ 𝐵 ∈ 𝑉 ) → ( sigAlgebra ‘ ∪ 𝐴 ) = ( sigAlgebra ‘ ∪ 𝐵 ) )
5	2 4	eleqtrrd	⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ 𝐴 ⊆ ( sigaGen ‘ 𝐵 ) ∧ 𝐵 ∈ 𝑉 ) → ( sigaGen ‘ 𝐵 ) ∈ ( sigAlgebra ‘ ∪ 𝐴 ) )
6		simp2	⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ 𝐴 ⊆ ( sigaGen ‘ 𝐵 ) ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ⊆ ( sigaGen ‘ 𝐵 ) )
7		sigagenss	⊢ ( ( ( sigaGen ‘ 𝐵 ) ∈ ( sigAlgebra ‘ ∪ 𝐴 ) ∧ 𝐴 ⊆ ( sigaGen ‘ 𝐵 ) ) → ( sigaGen ‘ 𝐴 ) ⊆ ( sigaGen ‘ 𝐵 ) )
8	5 6 7	syl2anc	⊢ ( ( ∪ 𝐴 = ∪ 𝐵 ∧ 𝐴 ⊆ ( sigaGen ‘ 𝐵 ) ∧ 𝐵 ∈ 𝑉 ) → ( sigaGen ‘ 𝐴 ) ⊆ ( sigaGen ‘ 𝐵 ) )