Metamath Proof Explorer

Theorem sxsigon

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

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

Proof

Step	Hyp	Ref	Expression
1		sxsiga	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to S \times_{s} T \in ⋃ ran sigAlgebra$
2		eqid	$⊢ ran (x \in S, y \in T ⟼ x \times y) = ran (x \in S, y \in T ⟼ x \times y)$
3		eqid	$⊢ ⋃ S = ⋃ S$
4		eqid	$⊢ ⋃ T = ⋃ T$
5	2 3 4	txuni2	$⊢ ⋃ S \times ⋃ T = ⋃ ran (x \in S, y \in T ⟼ x \times y)$
6	2	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))$
7	6	unieqd	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to ⋃ (S \times_{s} T) = ⋃ 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
8		mpoexga	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to (x \in S, y \in T ⟼ x \times y) \in V$
9		rnexg	$⊢ (x \in S, y \in T ⟼ x \times y) \in V \to ran (x \in S, y \in T ⟼ x \times y) \in V$
10		unisg	$⊢ ran (x \in S, y \in T ⟼ x \times y) \in V \to ⋃ 𝛔 (ran (x \in S, y \in T ⟼ x \times y)) = ⋃ ran (x \in S, y \in T ⟼ x \times y)$
11	8 9 10	3syl	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to ⋃ 𝛔 (ran (x \in S, y \in T ⟼ x \times y)) = ⋃ ran (x \in S, y \in T ⟼ x \times y)$
12	7 11	eqtrd	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to ⋃ (S \times_{s} T) = ⋃ ran (x \in S, y \in T ⟼ x \times y)$
13	5 12	eqtr4id	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to ⋃ S \times ⋃ T = ⋃ (S \times_{s} T)$
14		issgon	$⊢ S \times_{s} T \in sigAlgebra (⋃ S \times ⋃ T) \leftrightarrow (S \times_{s} T \in ⋃ ran sigAlgebra \land ⋃ S \times ⋃ T = ⋃ (S \times_{s} T))$
15	1 13 14	sylanbrc	$⊢ (S \in ⋃ ran sigAlgebra \land T \in ⋃ ran sigAlgebra) \to S \times_{s} T \in sigAlgebra (⋃ S \times ⋃ T)$