Metamath Proof Explorer

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 ⊢ ⋃ A = ⋃ B ∧ A ⊆ 𝛔 ⁡ B ∧ B ∈ V → 𝛔 ⁡ A ⊆ 𝛔 ⁡ B

Proof

Step Hyp Ref Expression
1 sigagensiga ⊢ B ∈ V → 𝛔 ⁡ B ∈ sigAlgebra ⁡ ⋃ B
2 1 3ad2ant3 ⊢ ⋃ A = ⋃ B ∧ A ⊆ 𝛔 ⁡ B ∧ B ∈ V → 𝛔 ⁡ B ∈ sigAlgebra ⁡ ⋃ B
3 simp1 ⊢ ⋃ A = ⋃ B ∧ A ⊆ 𝛔 ⁡ B ∧ B ∈ V → ⋃ A = ⋃ B
4 3 fveq2d ⊢ ⋃ A = ⋃ B ∧ A ⊆ 𝛔 ⁡ B ∧ B ∈ V → sigAlgebra ⁡ ⋃ A = sigAlgebra ⁡ ⋃ B
5 2 4 eleqtrrd ⊢ ⋃ A = ⋃ B ∧ A ⊆ 𝛔 ⁡ B ∧ B ∈ V → 𝛔 ⁡ B ∈ sigAlgebra ⁡ ⋃ A
6 simp2 ⊢ ⋃ A = ⋃ B ∧ A ⊆ 𝛔 ⁡ B ∧ B ∈ V → A ⊆ 𝛔 ⁡ B
7 sigagenss ⊢ 𝛔 ⁡ B ∈ sigAlgebra ⁡ ⋃ A ∧ A ⊆ 𝛔 ⁡ B → 𝛔 ⁡ A ⊆ 𝛔 ⁡ B
8 5 6 7 syl2anc ⊢ ⋃ A = ⋃ B ∧ A ⊆ 𝛔 ⁡ B ∧ B ∈ V → 𝛔 ⁡ A ⊆ 𝛔 ⁡ B