elsx

Description: The cartesian product of two open sets is an element of the product sigma-algebra. (Contributed by Thierry Arnoux, 3-Jun-2017)

		Ref	Expression
	Assertion	elsx	$⊢ ((S \in V \land T \in W) \land (A \in S \land B \in T)) \to A \times B \in (S \times_{s} T)$

Proof

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	txbasex	$⊢ (S \in V \land T \in W) \to ran (x \in S, y \in T ⟼ x \times y) \in V$
3		sssigagen	$⊢ ran (x \in S, y \in T ⟼ x \times y) \in V \to ran (x \in S, y \in T ⟼ x \times y) \subseteq 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
4	2 3	syl	$⊢ (S \in V \land T \in W) \to ran (x \in S, y \in T ⟼ x \times y) \subseteq 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
5	4	adantr	$⊢ ((S \in V \land T \in W) \land (A \in S \land B \in T)) \to ran (x \in S, y \in T ⟼ x \times y) \subseteq 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
6		eqid	$⊢ A \times B = A \times B$
7		xpeq1	$⊢ x = A \to x \times y = A \times y$
8	7	eqeq2d	$⊢ x = A \to (A \times B = x \times y \leftrightarrow A \times B = A \times y)$
9		xpeq2	$⊢ y = B \to A \times y = A \times B$
10	9	eqeq2d	$⊢ y = B \to (A \times B = A \times y \leftrightarrow A \times B = A \times B)$
11	8 10	rspc2ev	$⊢ (A \in S \land B \in T \land A \times B = A \times B) \to \exists x \in S \exists y \in T A \times B = x \times y$
12	6 11	mp3an3	$⊢ (A \in S \land B \in T) \to \exists x \in S \exists y \in T A \times B = x \times y$
13		xpexg	$⊢ (A \in S \land B \in T) \to A \times B \in V$
14		eqid	$⊢ (x \in S, y \in T ⟼ x \times y) = (x \in S, y \in T ⟼ x \times y)$
15	14	elrnmpog	$⊢ A \times B \in V \to (A \times B \in ran (x \in S, y \in T ⟼ x \times y) \leftrightarrow \exists x \in S \exists y \in T A \times B = x \times y)$
16	13 15	syl	$⊢ (A \in S \land B \in T) \to (A \times B \in ran (x \in S, y \in T ⟼ x \times y) \leftrightarrow \exists x \in S \exists y \in T A \times B = x \times y)$
17	12 16	mpbird	$⊢ (A \in S \land B \in T) \to A \times B \in ran (x \in S, y \in T ⟼ x \times y)$
18	17	adantl	$⊢ ((S \in V \land T \in W) \land (A \in S \land B \in T)) \to A \times B \in ran (x \in S, y \in T ⟼ x \times y)$
19	5 18	sseldd	$⊢ ((S \in V \land T \in W) \land (A \in S \land B \in T)) \to A \times B \in 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
20	1	sxval	$⊢ (S \in V \land T \in W) \to S \times_{s} T = 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
21	20	adantr	$⊢ ((S \in V \land T \in W) \land (A \in S \land B \in T)) \to S \times_{s} T = 𝛔 (ran (x \in S, y \in T ⟼ x \times y))$
22	19 21	eleqtrrd	$⊢ ((S \in V \land T \in W) \land (A \in S \land B \in T)) \to A \times B \in (S \times_{s} T)$

Metamath Proof Explorer

Theorem elsx

Proof