txbas

Description: The set of Cartesian products of elements from two topological bases is a basis. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 31-Aug-2015)

		Ref	Expression
	Hypothesis	txval.1	$⊢ B = ran (x \in R, y \in S ⟼ x \times y)$
	Assertion	txbas	$⊢ (R \in TopBases \land S \in TopBases) \to B \in TopBases$

Proof

Step	Hyp	Ref	Expression
1		txval.1	$⊢ B = ran (x \in R, y \in S ⟼ x \times y)$
2		xpeq1	$⊢ x = a \to x \times y = a \times y$
3		xpeq2	$⊢ y = b \to a \times y = a \times b$
4	2 3	cbvmpov	$⊢ (x \in R, y \in S ⟼ x \times y) = (a \in R, b \in S ⟼ a \times b)$
5	4	rnmpo	$⊢ ran (x \in R, y \in S ⟼ x \times y) = \{u \| \exists a \in R \exists b \in S u = a \times b\}$
6	1 5	eqtri	$⊢ B = \{u \| \exists a \in R \exists b \in S u = a \times b\}$
7	6	abeq2i	$⊢ u \in B \leftrightarrow \exists a \in R \exists b \in S u = a \times b$
8		xpeq1	$⊢ x = c \to x \times y = c \times y$
9		xpeq2	$⊢ y = d \to c \times y = c \times d$
10	8 9	cbvmpov	$⊢ (x \in R, y \in S ⟼ x \times y) = (c \in R, d \in S ⟼ c \times d)$
11	10	rnmpo	$⊢ ran (x \in R, y \in S ⟼ x \times y) = \{v \| \exists c \in R \exists d \in S v = c \times d\}$
12	1 11	eqtri	$⊢ B = \{v \| \exists c \in R \exists d \in S v = c \times d\}$
13	12	abeq2i	$⊢ v \in B \leftrightarrow \exists c \in R \exists d \in S v = c \times d$
14	7 13	anbi12i	$⊢ (u \in B \land v \in B) \leftrightarrow (\exists a \in R \exists b \in S u = a \times b \land \exists c \in R \exists d \in S v = c \times d)$
15		reeanv	$⊢ \exists a \in R \exists c \in R (\exists b \in S u = a \times b \land \exists d \in S v = c \times d) \leftrightarrow (\exists a \in R \exists b \in S u = a \times b \land \exists c \in R \exists d \in S v = c \times d)$
16	14 15	bitr4i	$⊢ (u \in B \land v \in B) \leftrightarrow \exists a \in R \exists c \in R (\exists b \in S u = a \times b \land \exists d \in S v = c \times d)$
17		reeanv	$⊢ \exists b \in S \exists d \in S (u = a \times b \land v = c \times d) \leftrightarrow (\exists b \in S u = a \times b \land \exists d \in S v = c \times d)$
18		basis2	$⊢ ((R \in TopBases \land a \in R) \land (c \in R \land u \in (a \cap c))) \to \exists x \in R (u \in x \land x \subseteq a \cap c)$
19	18	exp43	$⊢ R \in TopBases \to (a \in R \to (c \in R \to (u \in (a \cap c) \to \exists x \in R (u \in x \land x \subseteq a \cap c))))$
20	19	imp42	$⊢ ((R \in TopBases \land (a \in R \land c \in R)) \land u \in (a \cap c)) \to \exists x \in R (u \in x \land x \subseteq a \cap c)$
21		basis2	$⊢ ((S \in TopBases \land b \in S) \land (d \in S \land v \in (b \cap d))) \to \exists y \in S (v \in y \land y \subseteq b \cap d)$
22	21	exp43	$⊢ S \in TopBases \to (b \in S \to (d \in S \to (v \in (b \cap d) \to \exists y \in S (v \in y \land y \subseteq b \cap d))))$
23	22	imp42	$⊢ ((S \in TopBases \land (b \in S \land d \in S)) \land v \in (b \cap d)) \to \exists y \in S (v \in y \land y \subseteq b \cap d)$
24		reeanv	$⊢ \exists x \in R \exists y \in S ((u \in x \land x \subseteq a \cap c) \land (v \in y \land y \subseteq b \cap d)) \leftrightarrow (\exists x \in R (u \in x \land x \subseteq a \cap c) \land \exists y \in S (v \in y \land y \subseteq b \cap d))$
25		opelxpi	$⊢ (u \in x \land v \in y) \to ⟨u, v⟩ \in (x \times y)$
26		xpss12	$⊢ (x \subseteq a \cap c \land y \subseteq b \cap d) \to x \times y \subseteq (a \cap c) \times (b \cap d)$
27	25 26	anim12i	$⊢ ((u \in x \land v \in y) \land (x \subseteq a \cap c \land y \subseteq b \cap d)) \to (⟨u, v⟩ \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
28	27	an4s	$⊢ ((u \in x \land x \subseteq a \cap c) \land (v \in y \land y \subseteq b \cap d)) \to (⟨u, v⟩ \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
29	28	reximi	$⊢ \exists y \in S ((u \in x \land x \subseteq a \cap c) \land (v \in y \land y \subseteq b \cap d)) \to \exists y \in S (⟨u, v⟩ \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
30	29	reximi	$⊢ \exists x \in R \exists y \in S ((u \in x \land x \subseteq a \cap c) \land (v \in y \land y \subseteq b \cap d)) \to \exists x \in R \exists y \in S (⟨u, v⟩ \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
31	24 30	sylbir	$⊢ (\exists x \in R (u \in x \land x \subseteq a \cap c) \land \exists y \in S (v \in y \land y \subseteq b \cap d)) \to \exists x \in R \exists y \in S (⟨u, v⟩ \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
32	20 23 31	syl2an	$⊢ (((R \in TopBases \land (a \in R \land c \in R)) \land u \in (a \cap c)) \land ((S \in TopBases \land (b \in S \land d \in S)) \land v \in (b \cap d))) \to \exists x \in R \exists y \in S (⟨u, v⟩ \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
33	32	an4s	$⊢ (((R \in TopBases \land (a \in R \land c \in R)) \land (S \in TopBases \land (b \in S \land d \in S))) \land (u \in (a \cap c) \land v \in (b \cap d))) \to \exists x \in R \exists y \in S (⟨u, v⟩ \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
34	33	ralrimivva	$⊢ ((R \in TopBases \land (a \in R \land c \in R)) \land (S \in TopBases \land (b \in S \land d \in S))) \to \forall u \in (a \cap c) \forall v \in (b \cap d) \exists x \in R \exists y \in S (⟨u, v⟩ \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
35		eleq1	$⊢ p = ⟨u, v⟩ \to (p \in (x \times y) \leftrightarrow ⟨u, v⟩ \in (x \times y))$
36	35	anbi1d	$⊢ p = ⟨u, v⟩ \to ((p \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d)) \leftrightarrow (⟨u, v⟩ \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d)))$
37	36	2rexbidv	$⊢ p = ⟨u, v⟩ \to (\exists x \in R \exists y \in S (p \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d)) \leftrightarrow \exists x \in R \exists y \in S (⟨u, v⟩ \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d)))$
38	37	ralxp	$⊢ \forall p \in ((a \cap c) \times (b \cap d)) \exists x \in R \exists y \in S (p \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d)) \leftrightarrow \forall u \in (a \cap c) \forall v \in (b \cap d) \exists x \in R \exists y \in S (⟨u, v⟩ \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
39	34 38	sylibr	$⊢ ((R \in TopBases \land (a \in R \land c \in R)) \land (S \in TopBases \land (b \in S \land d \in S))) \to \forall p \in ((a \cap c) \times (b \cap d)) \exists x \in R \exists y \in S (p \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
40	39	an4s	$⊢ ((R \in TopBases \land S \in TopBases) \land ((a \in R \land c \in R) \land (b \in S \land d \in S))) \to \forall p \in ((a \cap c) \times (b \cap d)) \exists x \in R \exists y \in S (p \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
41	40	anassrs	$⊢ (((R \in TopBases \land S \in TopBases) \land (a \in R \land c \in R)) \land (b \in S \land d \in S)) \to \forall p \in ((a \cap c) \times (b \cap d)) \exists x \in R \exists y \in S (p \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
42		ineq12	$⊢ (u = a \times b \land v = c \times d) \to u \cap v = (a \times b) \cap (c \times d)$
43		inxp	$⊢ (a \times b) \cap (c \times d) = (a \cap c) \times (b \cap d)$
44	42 43	syl6eq	$⊢ (u = a \times b \land v = c \times d) \to u \cap v = (a \cap c) \times (b \cap d)$
45	44	sseq2d	$⊢ (u = a \times b \land v = c \times d) \to (t \subseteq u \cap v \leftrightarrow t \subseteq (a \cap c) \times (b \cap d))$
46	45	anbi2d	$⊢ (u = a \times b \land v = c \times d) \to ((p \in t \land t \subseteq u \cap v) \leftrightarrow (p \in t \land t \subseteq (a \cap c) \times (b \cap d)))$
47	46	rexbidv	$⊢ (u = a \times b \land v = c \times d) \to (\exists t \in B (p \in t \land t \subseteq u \cap v) \leftrightarrow \exists t \in B (p \in t \land t \subseteq (a \cap c) \times (b \cap d)))$
48	1	rexeqi	$⊢ \exists t \in B (p \in t \land t \subseteq (a \cap c) \times (b \cap d)) \leftrightarrow \exists t \in ran (x \in R, y \in S ⟼ x \times y) (p \in t \land t \subseteq (a \cap c) \times (b \cap d))$
49		fvex	$⊢ 1^{st} (z) \in V$
50		fvex	$⊢ 2^{nd} (z) \in V$
51	49 50	xpex	$⊢ 1^{st} (z) \times 2^{nd} (z) \in V$
52	51	rgenw	$⊢ \forall z \in (R \times S) 1^{st} (z) \times 2^{nd} (z) \in V$
53		vex	$⊢ x \in V$
54		vex	$⊢ y \in V$
55	53 54	op1std	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) = x$
56	53 54	op2ndd	$⊢ z = ⟨x, y⟩ \to 2^{nd} (z) = y$
57	55 56	xpeq12d	$⊢ z = ⟨x, y⟩ \to 1^{st} (z) \times 2^{nd} (z) = x \times y$
58	57	mpompt	$⊢ (z \in (R \times S) ⟼ 1^{st} (z) \times 2^{nd} (z)) = (x \in R, y \in S ⟼ x \times y)$
59	58	eqcomi	$⊢ (x \in R, y \in S ⟼ x \times y) = (z \in (R \times S) ⟼ 1^{st} (z) \times 2^{nd} (z))$
60		eleq2	$⊢ t = 1^{st} (z) \times 2^{nd} (z) \to (p \in t \leftrightarrow p \in (1^{st} (z) \times 2^{nd} (z)))$
61		sseq1	$⊢ t = 1^{st} (z) \times 2^{nd} (z) \to (t \subseteq (a \cap c) \times (b \cap d) \leftrightarrow 1^{st} (z) \times 2^{nd} (z) \subseteq (a \cap c) \times (b \cap d))$
62	60 61	anbi12d	$⊢ t = 1^{st} (z) \times 2^{nd} (z) \to ((p \in t \land t \subseteq (a \cap c) \times (b \cap d)) \leftrightarrow (p \in (1^{st} (z) \times 2^{nd} (z)) \land 1^{st} (z) \times 2^{nd} (z) \subseteq (a \cap c) \times (b \cap d)))$
63	59 62	rexrnmptw	$⊢ \forall z \in (R \times S) 1^{st} (z) \times 2^{nd} (z) \in V \to (\exists t \in ran (x \in R, y \in S ⟼ x \times y) (p \in t \land t \subseteq (a \cap c) \times (b \cap d)) \leftrightarrow \exists z \in (R \times S) (p \in (1^{st} (z) \times 2^{nd} (z)) \land 1^{st} (z) \times 2^{nd} (z) \subseteq (a \cap c) \times (b \cap d)))$
64	52 63	ax-mp	$⊢ \exists t \in ran (x \in R, y \in S ⟼ x \times y) (p \in t \land t \subseteq (a \cap c) \times (b \cap d)) \leftrightarrow \exists z \in (R \times S) (p \in (1^{st} (z) \times 2^{nd} (z)) \land 1^{st} (z) \times 2^{nd} (z) \subseteq (a \cap c) \times (b \cap d))$
65	57	eleq2d	$⊢ z = ⟨x, y⟩ \to (p \in (1^{st} (z) \times 2^{nd} (z)) \leftrightarrow p \in (x \times y))$
66	57	sseq1d	$⊢ z = ⟨x, y⟩ \to (1^{st} (z) \times 2^{nd} (z) \subseteq (a \cap c) \times (b \cap d) \leftrightarrow x \times y \subseteq (a \cap c) \times (b \cap d))$
67	65 66	anbi12d	$⊢ z = ⟨x, y⟩ \to ((p \in (1^{st} (z) \times 2^{nd} (z)) \land 1^{st} (z) \times 2^{nd} (z) \subseteq (a \cap c) \times (b \cap d)) \leftrightarrow (p \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d)))$
68	67	rexxp	$⊢ \exists z \in (R \times S) (p \in (1^{st} (z) \times 2^{nd} (z)) \land 1^{st} (z) \times 2^{nd} (z) \subseteq (a \cap c) \times (b \cap d)) \leftrightarrow \exists x \in R \exists y \in S (p \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
69	48 64 68	3bitri	$⊢ \exists t \in B (p \in t \land t \subseteq (a \cap c) \times (b \cap d)) \leftrightarrow \exists x \in R \exists y \in S (p \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d))$
70	47 69	syl6bb	$⊢ (u = a \times b \land v = c \times d) \to (\exists t \in B (p \in t \land t \subseteq u \cap v) \leftrightarrow \exists x \in R \exists y \in S (p \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d)))$
71	44 70	raleqbidv	$⊢ (u = a \times b \land v = c \times d) \to (\forall p \in (u \cap v) \exists t \in B (p \in t \land t \subseteq u \cap v) \leftrightarrow \forall p \in ((a \cap c) \times (b \cap d)) \exists x \in R \exists y \in S (p \in (x \times y) \land x \times y \subseteq (a \cap c) \times (b \cap d)))$
72	41 71	syl5ibrcom	$⊢ (((R \in TopBases \land S \in TopBases) \land (a \in R \land c \in R)) \land (b \in S \land d \in S)) \to ((u = a \times b \land v = c \times d) \to \forall p \in (u \cap v) \exists t \in B (p \in t \land t \subseteq u \cap v))$
73	72	rexlimdvva	$⊢ ((R \in TopBases \land S \in TopBases) \land (a \in R \land c \in R)) \to (\exists b \in S \exists d \in S (u = a \times b \land v = c \times d) \to \forall p \in (u \cap v) \exists t \in B (p \in t \land t \subseteq u \cap v))$
74	17 73	syl5bir	$⊢ ((R \in TopBases \land S \in TopBases) \land (a \in R \land c \in R)) \to ((\exists b \in S u = a \times b \land \exists d \in S v = c \times d) \to \forall p \in (u \cap v) \exists t \in B (p \in t \land t \subseteq u \cap v))$
75	74	rexlimdvva	$⊢ (R \in TopBases \land S \in TopBases) \to (\exists a \in R \exists c \in R (\exists b \in S u = a \times b \land \exists d \in S v = c \times d) \to \forall p \in (u \cap v) \exists t \in B (p \in t \land t \subseteq u \cap v))$
76	16 75	syl5bi	$⊢ (R \in TopBases \land S \in TopBases) \to ((u \in B \land v \in B) \to \forall p \in (u \cap v) \exists t \in B (p \in t \land t \subseteq u \cap v))$
77	76	ralrimivv	$⊢ (R \in TopBases \land S \in TopBases) \to \forall u \in B \forall v \in B \forall p \in (u \cap v) \exists t \in B (p \in t \land t \subseteq u \cap v)$
78	1	txbasex	$⊢ (R \in TopBases \land S \in TopBases) \to B \in V$
79		isbasis2g	$⊢ B \in V \to (B \in TopBases \leftrightarrow \forall u \in B \forall v \in B \forall p \in (u \cap v) \exists t \in B (p \in t \land t \subseteq u \cap v))$
80	78 79	syl	$⊢ (R \in TopBases \land S \in TopBases) \to (B \in TopBases \leftrightarrow \forall u \in B \forall v \in B \forall p \in (u \cap v) \exists t \in B (p \in t \land t \subseteq u \cap v))$
81	77 80	mpbird	$⊢ (R \in TopBases \land S \in TopBases) \to B \in TopBases$

Metamath Proof Explorer

Theorem txbas

Proof