sxsiga

Description: A product sigma-algebra is a sigma-algebra. (Contributed by Thierry Arnoux, 1-Jun-2017)

		Ref	Expression
	Assertion	sxsiga	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to S \times_{s} T \in ⋃ ran sigAlgebra$

Step	Hyp	Ref	Expression
1		eqid	$⊢ ran (x \in S, y \in T ⟼ x \times y) = ran (x \in S, y \in T ⟼ x \times y)$
2	1	sxval	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to S \times_{s} T = 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
3	1	txbasex	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to ran (x \in S, y \in T ⟼ x \times y) \in V$
4		sigagensiga	$⊢ ran (x \in S, y \in T ⟼ x \times y) \in V \to 𝛔 (ran (x \in S, y \in T ⟼ x \times y)) \in sigAlgebra (⋃ ran (x \in S, y \in T ⟼ x \times y))$
5	3 4	syl	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to 𝛔 (ran (x \in S, y \in T ⟼ x \times y)) \in sigAlgebra (⋃ ran (x \in S, y \in T ⟼ x \times y))$
6	2 5	eqeltrd	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to S \times_{s} T \in sigAlgebra (⋃ ran (x \in S, y \in T ⟼ x \times y))$
7		elrnsiga	$⊢ S \times_{s} T \in sigAlgebra (⋃ ran (x \in S, y \in T ⟼ x \times y)) \to S \times_{s} T \in ⋃ ran sigAlgebra$
8	6 7	syl	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to S \times_{s} T \in ⋃ ran sigAlgebra$

Metamath Proof Explorer