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 
|- ( ( U. A = U. B /\ A C_ ( sigaGen ` B ) /\ B e. V ) -> ( sigaGen ` A ) C_ ( sigaGen ` B ) )

Proof

Step Hyp Ref Expression
1 sigagensiga 
 |-  ( B e. V -> ( sigaGen ` B ) e. ( sigAlgebra ` U. B ) )
2 1 3ad2ant3 
 |-  ( ( U. A = U. B /\ A C_ ( sigaGen ` B ) /\ B e. V ) -> ( sigaGen ` B ) e. ( sigAlgebra ` U. B ) )
3 simp1 
 |-  ( ( U. A = U. B /\ A C_ ( sigaGen ` B ) /\ B e. V ) -> U. A = U. B )
4 3 fveq2d 
 |-  ( ( U. A = U. B /\ A C_ ( sigaGen ` B ) /\ B e. V ) -> ( sigAlgebra ` U. A ) = ( sigAlgebra ` U. B ) )
5 2 4 eleqtrrd 
 |-  ( ( U. A = U. B /\ A C_ ( sigaGen ` B ) /\ B e. V ) -> ( sigaGen ` B ) e. ( sigAlgebra ` U. A ) )
6 simp2 
 |-  ( ( U. A = U. B /\ A C_ ( sigaGen ` B ) /\ B e. V ) -> A C_ ( sigaGen ` B ) )
7 sigagenss 
 |-  ( ( ( sigaGen ` B ) e. ( sigAlgebra ` U. A ) /\ A C_ ( sigaGen ` B ) ) -> ( sigaGen ` A ) C_ ( sigaGen ` B ) )
8 5 6 7 syl2anc 
 |-  ( ( U. A = U. B /\ A C_ ( sigaGen ` B ) /\ B e. V ) -> ( sigaGen ` A ) C_ ( sigaGen ` B ) )