txopn

Description: The product of two open sets is open in the product topology. (Contributed by Jeff Madsen, 2-Sep-2009)

		Ref	Expression
	Assertion	txopn	$⊢ ((R \in V \land S \in W) \land (A \in R \land B \in S)) \to A \times B \in (R \times_{t} S)$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ ran (u \in R, v \in S ⟼ u \times v) = ran (u \in R, v \in S ⟼ u \times v)$
2	1	txbasex	$⊢ (R \in V \land S \in W) \to ran (u \in R, v \in S ⟼ u \times v) \in V$
3		bastg	$⊢ ran (u \in R, v \in S ⟼ u \times v) \in V \to ran (u \in R, v \in S ⟼ u \times v) \subseteq topGen (ran (u \in R, v \in S ⟼ u \times v))$
4	2 3	syl	$⊢ (R \in V \land S \in W) \to ran (u \in R, v \in S ⟼ u \times v) \subseteq topGen (ran (u \in R, v \in S ⟼ u \times v))$
5	4	adantr	$⊢ ((R \in V \land S \in W) \land (A \in R \land B \in S)) \to ran (u \in R, v \in S ⟼ u \times v) \subseteq topGen (ran (u \in R, v \in S ⟼ u \times v))$
6		eqid	$⊢ A \times B = A \times B$
7		xpeq1	$⊢ u = A \to u \times v = A \times v$
8	7	eqeq2d	$⊢ u = A \to (A \times B = u \times v \leftrightarrow A \times B = A \times v)$
9		xpeq2	$⊢ v = B \to A \times v = A \times B$
10	9	eqeq2d	$⊢ v = B \to (A \times B = A \times v \leftrightarrow A \times B = A \times B)$
11	8 10	rspc2ev	$⊢ (A \in R \land B \in S \land A \times B = A \times B) \to \exists u \in R \exists v \in S A \times B = u \times v$
12	6 11	mp3an3	$⊢ (A \in R \land B \in S) \to \exists u \in R \exists v \in S A \times B = u \times v$
13		xpexg	$⊢ (A \in R \land B \in S) \to A \times B \in V$
14		eqid	$⊢ (u \in R, v \in S ⟼ u \times v) = (u \in R, v \in S ⟼ u \times v)$
15	14	elrnmpog	$⊢ A \times B \in V \to (A \times B \in ran (u \in R, v \in S ⟼ u \times v) \leftrightarrow \exists u \in R \exists v \in S A \times B = u \times v)$
16	13 15	syl	$⊢ (A \in R \land B \in S) \to (A \times B \in ran (u \in R, v \in S ⟼ u \times v) \leftrightarrow \exists u \in R \exists v \in S A \times B = u \times v)$
17	12 16	mpbird	$⊢ (A \in R \land B \in S) \to A \times B \in ran (u \in R, v \in S ⟼ u \times v)$
18	17	adantl	$⊢ ((R \in V \land S \in W) \land (A \in R \land B \in S)) \to A \times B \in ran (u \in R, v \in S ⟼ u \times v)$
19	5 18	sseldd	$⊢ ((R \in V \land S \in W) \land (A \in R \land B \in S)) \to A \times B \in topGen (ran (u \in R, v \in S ⟼ u \times v))$
20	1	txval	$⊢ (R \in V \land S \in W) \to R \times_{t} S = topGen (ran (u \in R, v \in S ⟼ u \times v))$
21	20	adantr	$⊢ ((R \in V \land S \in W) \land (A \in R \land B \in S)) \to R \times_{t} S = topGen (ran (u \in R, v \in S ⟼ u \times v))$
22	19 21	eleqtrrd	$⊢ ((R \in V \land S \in W) \land (A \in R \land B \in S)) \to A \times B \in (R \times_{t} S)$

Metamath Proof Explorer

Theorem txopn

Proof