txbasval

Description: It is sufficient to consider products of the bases for the topologies in the topological product. (Contributed by Mario Carneiro, 25-Aug-2014)

		Ref	Expression
	Assertion	txbasval	$⊢ (R \in V \land S \in W) \to topGen (R) \times_{t} topGen (S) = 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	txval	$⊢ (R \in V \land S \in W) \to R \times_{t} S = topGen (ran (u \in R, v \in S ⟼ u \times v))$
3		bastg	$⊢ R \in V \to R \subseteq topGen (R)$
4		bastg	$⊢ S \in W \to S \subseteq topGen (S)$
5		resmpo	$⊢ (R \subseteq topGen (R) \land S \subseteq topGen (S)) \to {(u \in topGen (R), v \in topGen (S) ⟼ u \times v) ↾}_{(R \times S)} = (u \in R, v \in S ⟼ u \times v)$
6	3 4 5	syl2an	$⊢ (R \in V \land S \in W) \to {(u \in topGen (R), v \in topGen (S) ⟼ u \times v) ↾}_{(R \times S)} = (u \in R, v \in S ⟼ u \times v)$
7		resss	$⊢ {(u \in topGen (R), v \in topGen (S) ⟼ u \times v) ↾}_{(R \times S)} \subseteq (u \in topGen (R), v \in topGen (S) ⟼ u \times v)$
8	6 7	eqsstrrdi	$⊢ (R \in V \land S \in W) \to (u \in R, v \in S ⟼ u \times v) \subseteq (u \in topGen (R), v \in topGen (S) ⟼ u \times v)$
9		rnss	$⊢ (u \in R, v \in S ⟼ u \times v) \subseteq (u \in topGen (R), v \in topGen (S) ⟼ u \times v) \to ran (u \in R, v \in S ⟼ u \times v) \subseteq ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v)$
10	8 9	syl	$⊢ (R \in V \land S \in W) \to ran (u \in R, v \in S ⟼ u \times v) \subseteq ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v)$
11		eltg3	$⊢ R \in V \to (u \in topGen (R) \leftrightarrow \exists m (m \subseteq R \land u = ⋃ m))$
12		eltg3	$⊢ S \in W \to (v \in topGen (S) \leftrightarrow \exists n (n \subseteq S \land v = ⋃ n))$
13	11 12	bi2anan9	$⊢ (R \in V \land S \in W) \to ((u \in topGen (R) \land v \in topGen (S)) \leftrightarrow (\exists m (m \subseteq R \land u = ⋃ m) \land \exists n (n \subseteq S \land v = ⋃ n)))$
14		exdistrv	$⊢ \exists m \exists n ((m \subseteq R \land u = ⋃ m) \land (n \subseteq S \land v = ⋃ n)) \leftrightarrow (\exists m (m \subseteq R \land u = ⋃ m) \land \exists n (n \subseteq S \land v = ⋃ n))$
15		an4	$⊢ ((m \subseteq R \land u = ⋃ m) \land (n \subseteq S \land v = ⋃ n)) \leftrightarrow ((m \subseteq R \land n \subseteq S) \land (u = ⋃ m \land v = ⋃ n))$
16		uniiun	$⊢ ⋃ m = ⋃_{x \in m} x$
17		uniiun	$⊢ ⋃ n = ⋃_{y \in n} y$
18	16 17	xpeq12i	$⊢ ⋃ m \times ⋃ n = ⋃_{x \in m} x \times ⋃_{y \in n} y$
19		xpiundir	$⊢ ⋃_{x \in m} x \times ⋃_{y \in n} y = ⋃_{x \in m} (x \times ⋃_{y \in n} y)$
20		xpiundi	$⊢ x \times ⋃_{y \in n} y = ⋃_{y \in n} (x \times y)$
21	20	a1i	$⊢ x \in m \to x \times ⋃_{y \in n} y = ⋃_{y \in n} (x \times y)$
22	21	iuneq2i	$⊢ ⋃_{x \in m} (x \times ⋃_{y \in n} y) = ⋃_{x \in m} ⋃_{y \in n} (x \times y)$
23	18 19 22	3eqtri	$⊢ ⋃ m \times ⋃ n = ⋃_{x \in m} ⋃_{y \in n} (x \times y)$
24		ovex	$⊢ R \times_{t} S \in V$
25		ssel2	$⊢ (m \subseteq R \land x \in m) \to x \in R$
26		ssel2	$⊢ (n \subseteq S \land y \in n) \to y \in S$
27	25 26	anim12i	$⊢ ((m \subseteq R \land x \in m) \land (n \subseteq S \land y \in n)) \to (x \in R \land y \in S)$
28	27	an4s	$⊢ ((m \subseteq R \land n \subseteq S) \land (x \in m \land y \in n)) \to (x \in R \land y \in S)$
29		txopn	$⊢ ((R \in V \land S \in W) \land (x \in R \land y \in S)) \to x \times y \in (R \times_{t} S)$
30	28 29	sylan2	$⊢ ((R \in V \land S \in W) \land ((m \subseteq R \land n \subseteq S) \land (x \in m \land y \in n))) \to x \times y \in (R \times_{t} S)$
31	30	anassrs	$⊢ (((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \land (x \in m \land y \in n)) \to x \times y \in (R \times_{t} S)$
32	31	anassrs	$⊢ ((((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \land x \in m) \land y \in n) \to x \times y \in (R \times_{t} S)$
33	32	ralrimiva	$⊢ (((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \land x \in m) \to \forall y \in n x \times y \in (R \times_{t} S)$
34		tgiun	$⊢ (R \times_{t} S \in V \land \forall y \in n x \times y \in (R \times_{t} S)) \to ⋃_{y \in n} (x \times y) \in topGen (R \times_{t} S)$
35	24 33 34	sylancr	$⊢ (((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \land x \in m) \to ⋃_{y \in n} (x \times y) \in topGen (R \times_{t} S)$
36	1	txbasex	$⊢ (R \in V \land S \in W) \to ran (u \in R, v \in S ⟼ u \times v) \in V$
37		tgidm	$⊢ ran (u \in R, v \in S ⟼ u \times v) \in V \to topGen (topGen (ran (u \in R, v \in S ⟼ u \times v))) = topGen (ran (u \in R, v \in S ⟼ u \times v))$
38	36 37	syl	$⊢ (R \in V \land S \in W) \to topGen (topGen (ran (u \in R, v \in S ⟼ u \times v))) = topGen (ran (u \in R, v \in S ⟼ u \times v))$
39	2	fveq2d	$⊢ (R \in V \land S \in W) \to topGen (R \times_{t} S) = topGen (topGen (ran (u \in R, v \in S ⟼ u \times v)))$
40	38 39 2	3eqtr4d	$⊢ (R \in V \land S \in W) \to topGen (R \times_{t} S) = R \times_{t} S$
41	40	adantr	$⊢ ((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \to topGen (R \times_{t} S) = R \times_{t} S$
42	41	adantr	$⊢ (((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \land x \in m) \to topGen (R \times_{t} S) = R \times_{t} S$
43	35 42	eleqtrd	$⊢ (((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \land x \in m) \to ⋃_{y \in n} (x \times y) \in (R \times_{t} S)$
44	43	ralrimiva	$⊢ ((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \to \forall x \in m ⋃_{y \in n} (x \times y) \in (R \times_{t} S)$
45		tgiun	$⊢ (R \times_{t} S \in V \land \forall x \in m ⋃_{y \in n} (x \times y) \in (R \times_{t} S)) \to ⋃_{x \in m} ⋃_{y \in n} (x \times y) \in topGen (R \times_{t} S)$
46	24 44 45	sylancr	$⊢ ((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \to ⋃_{x \in m} ⋃_{y \in n} (x \times y) \in topGen (R \times_{t} S)$
47	46 41	eleqtrd	$⊢ ((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \to ⋃_{x \in m} ⋃_{y \in n} (x \times y) \in (R \times_{t} S)$
48	23 47	eqeltrid	$⊢ ((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \to ⋃ m \times ⋃ n \in (R \times_{t} S)$
49		xpeq12	$⊢ (u = ⋃ m \land v = ⋃ n) \to u \times v = ⋃ m \times ⋃ n$
50	49	eleq1d	$⊢ (u = ⋃ m \land v = ⋃ n) \to (u \times v \in (R \times_{t} S) \leftrightarrow ⋃ m \times ⋃ n \in (R \times_{t} S))$
51	48 50	syl5ibrcom	$⊢ ((R \in V \land S \in W) \land (m \subseteq R \land n \subseteq S)) \to ((u = ⋃ m \land v = ⋃ n) \to u \times v \in (R \times_{t} S))$
52	51	expimpd	$⊢ (R \in V \land S \in W) \to (((m \subseteq R \land n \subseteq S) \land (u = ⋃ m \land v = ⋃ n)) \to u \times v \in (R \times_{t} S))$
53	15 52	syl5bi	$⊢ (R \in V \land S \in W) \to (((m \subseteq R \land u = ⋃ m) \land (n \subseteq S \land v = ⋃ n)) \to u \times v \in (R \times_{t} S))$
54	53	exlimdvv	$⊢ (R \in V \land S \in W) \to (\exists m \exists n ((m \subseteq R \land u = ⋃ m) \land (n \subseteq S \land v = ⋃ n)) \to u \times v \in (R \times_{t} S))$
55	14 54	syl5bir	$⊢ (R \in V \land S \in W) \to ((\exists m (m \subseteq R \land u = ⋃ m) \land \exists n (n \subseteq S \land v = ⋃ n)) \to u \times v \in (R \times_{t} S))$
56	13 55	sylbid	$⊢ (R \in V \land S \in W) \to ((u \in topGen (R) \land v \in topGen (S)) \to u \times v \in (R \times_{t} S))$
57	56	ralrimivv	$⊢ (R \in V \land S \in W) \to \forall u \in topGen (R) \forall v \in topGen (S) u \times v \in (R \times_{t} S)$
58		eqid	$⊢ (u \in topGen (R), v \in topGen (S) ⟼ u \times v) = (u \in topGen (R), v \in topGen (S) ⟼ u \times v)$
59	58	fmpo	$⊢ \forall u \in topGen (R) \forall v \in topGen (S) u \times v \in (R \times_{t} S) \leftrightarrow (u \in topGen (R), v \in topGen (S) ⟼ u \times v) : topGen (R) \times topGen (S) ⟶ R \times_{t} S$
60	57 59	sylib	$⊢ (R \in V \land S \in W) \to (u \in topGen (R), v \in topGen (S) ⟼ u \times v) : topGen (R) \times topGen (S) ⟶ R \times_{t} S$
61	60	frnd	$⊢ (R \in V \land S \in W) \to ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v) \subseteq R \times_{t} S$
62	61 2	sseqtrd	$⊢ (R \in V \land S \in W) \to ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v) \subseteq topGen (ran (u \in R, v \in S ⟼ u \times v))$
63		2basgen	$⊢ (ran (u \in R, v \in S ⟼ u \times v) \subseteq ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v) \land ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v) \subseteq topGen (ran (u \in R, v \in S ⟼ u \times v))) \to topGen (ran (u \in R, v \in S ⟼ u \times v)) = topGen (ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v))$
64	10 62 63	syl2anc	$⊢ (R \in V \land S \in W) \to topGen (ran (u \in R, v \in S ⟼ u \times v)) = topGen (ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v))$
65		fvex	$⊢ topGen (R) \in V$
66		fvex	$⊢ topGen (S) \in V$
67		eqid	$⊢ ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v) = ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v)$
68	67	txval	$⊢ (topGen (R) \in V \land topGen (S) \in V) \to topGen (R) \times_{t} topGen (S) = topGen (ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v))$
69	65 66 68	mp2an	$⊢ topGen (R) \times_{t} topGen (S) = topGen (ran (u \in topGen (R), v \in topGen (S) ⟼ u \times v))$
70	64 69	eqtr4di	$⊢ (R \in V \land S \in W) \to topGen (ran (u \in R, v \in S ⟼ u \times v)) = topGen (R) \times_{t} topGen (S)$
71	2 70	eqtr2d	$⊢ (R \in V \land S \in W) \to topGen (R) \times_{t} topGen (S) = R \times_{t} S$

Metamath Proof Explorer

Theorem txbasval

Proof