neitx

Description: The Cartesian product of two neighborhoods is a neighborhood in the product topology. (Contributed by Thierry Arnoux, 13-Jan-2018)

	Ref	Expression
Hypotheses	neitx.x	$⊢ X = ⋃ J$
	neitx.y	$⊢ Y = ⋃ K$
Assertion	neitx	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to A \times B \in nei (J \times_{t} K) (C \times D)$

Proof

Step	Hyp	Ref	Expression
1		neitx.x	$⊢ X = ⋃ J$
2		neitx.y	$⊢ Y = ⋃ K$
3	1	neii1	$⊢ (J \in Top \land A \in nei (J) (C)) \to A \subseteq X$
4	3	ad2ant2r	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to A \subseteq X$
5	2	neii1	$⊢ (K \in Top \land B \in nei (K) (D)) \to B \subseteq Y$
6	5	ad2ant2l	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to B \subseteq Y$
7		xpss12	$⊢ (A \subseteq X \land B \subseteq Y) \to A \times B \subseteq X \times Y$
8	4 6 7	syl2anc	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to A \times B \subseteq X \times Y$
9	1 2	txuni	$⊢ (J \in Top \land K \in Top) \to X \times Y = ⋃ (J \times_{t} K)$
10	9	adantr	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to X \times Y = ⋃ (J \times_{t} K)$
11	8 10	sseqtrd	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to A \times B \subseteq ⋃ (J \times_{t} K)$
12		simp-5l	$⊢ ((((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \land b \in K) \land (D \subseteq b \land b \subseteq B)) \to (J \in Top \land K \in Top)$
13		simp-4r	$⊢ ((((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \land b \in K) \land (D \subseteq b \land b \subseteq B)) \to a \in J$
14		simplr	$⊢ ((((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \land b \in K) \land (D \subseteq b \land b \subseteq B)) \to b \in K$
15		txopn	$⊢ ((J \in Top \land K \in Top) \land (a \in J \land b \in K)) \to a \times b \in (J \times_{t} K)$
16	12 13 14 15	syl12anc	$⊢ ((((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \land b \in K) \land (D \subseteq b \land b \subseteq B)) \to a \times b \in (J \times_{t} K)$
17		simpr1l	$⊢ ((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land ((C \subseteq a \land a \subseteq A) \land b \in K \land (D \subseteq b \land b \subseteq B))) \to C \subseteq a$
18	17	3anassrs	$⊢ ((((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \land b \in K) \land (D \subseteq b \land b \subseteq B)) \to C \subseteq a$
19		simprl	$⊢ ((((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \land b \in K) \land (D \subseteq b \land b \subseteq B)) \to D \subseteq b$
20		xpss12	$⊢ (C \subseteq a \land D \subseteq b) \to C \times D \subseteq a \times b$
21	18 19 20	syl2anc	$⊢ ((((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \land b \in K) \land (D \subseteq b \land b \subseteq B)) \to C \times D \subseteq a \times b$
22		simpr1r	$⊢ ((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land ((C \subseteq a \land a \subseteq A) \land b \in K \land (D \subseteq b \land b \subseteq B))) \to a \subseteq A$
23	22	3anassrs	$⊢ ((((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \land b \in K) \land (D \subseteq b \land b \subseteq B)) \to a \subseteq A$
24		simprr	$⊢ ((((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \land b \in K) \land (D \subseteq b \land b \subseteq B)) \to b \subseteq B$
25		xpss12	$⊢ (a \subseteq A \land b \subseteq B) \to a \times b \subseteq A \times B$
26	23 24 25	syl2anc	$⊢ ((((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \land b \in K) \land (D \subseteq b \land b \subseteq B)) \to a \times b \subseteq A \times B$
27		sseq2	$⊢ c = a \times b \to (C \times D \subseteq c \leftrightarrow C \times D \subseteq a \times b)$
28		sseq1	$⊢ c = a \times b \to (c \subseteq A \times B \leftrightarrow a \times b \subseteq A \times B)$
29	27 28	anbi12d	$⊢ c = a \times b \to ((C \times D \subseteq c \land c \subseteq A \times B) \leftrightarrow (C \times D \subseteq a \times b \land a \times b \subseteq A \times B))$
30	29	rspcev	$⊢ (a \times b \in (J \times_{t} K) \land (C \times D \subseteq a \times b \land a \times b \subseteq A \times B)) \to \exists c \in (J \times_{t} K) (C \times D \subseteq c \land c \subseteq A \times B)$
31	16 21 26 30	syl12anc	$⊢ ((((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \land b \in K) \land (D \subseteq b \land b \subseteq B)) \to \exists c \in (J \times_{t} K) (C \times D \subseteq c \land c \subseteq A \times B)$
32		neii2	$⊢ (K \in Top \land B \in nei (K) (D)) \to \exists b \in K (D \subseteq b \land b \subseteq B)$
33	32	ad2ant2l	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to \exists b \in K (D \subseteq b \land b \subseteq B)$
34	33	ad2antrr	$⊢ ((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \to \exists b \in K (D \subseteq b \land b \subseteq B)$
35	31 34	r19.29a	$⊢ ((((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \land a \in J) \land (C \subseteq a \land a \subseteq A)) \to \exists c \in (J \times_{t} K) (C \times D \subseteq c \land c \subseteq A \times B)$
36		neii2	$⊢ (J \in Top \land A \in nei (J) (C)) \to \exists a \in J (C \subseteq a \land a \subseteq A)$
37	36	ad2ant2r	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to \exists a \in J (C \subseteq a \land a \subseteq A)$
38	35 37	r19.29a	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to \exists c \in (J \times_{t} K) (C \times D \subseteq c \land c \subseteq A \times B)$
39		txtop	$⊢ (J \in Top \land K \in Top) \to J \times_{t} K \in Top$
40	39	adantr	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to J \times_{t} K \in Top$
41	1	neiss2	$⊢ (J \in Top \land A \in nei (J) (C)) \to C \subseteq X$
42	41	ad2ant2r	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to C \subseteq X$
43	2	neiss2	$⊢ (K \in Top \land B \in nei (K) (D)) \to D \subseteq Y$
44	43	ad2ant2l	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to D \subseteq Y$
45		xpss12	$⊢ (C \subseteq X \land D \subseteq Y) \to C \times D \subseteq X \times Y$
46	42 44 45	syl2anc	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to C \times D \subseteq X \times Y$
47	46 10	sseqtrd	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to C \times D \subseteq ⋃ (J \times_{t} K)$
48		eqid	$⊢ ⋃ (J \times_{t} K) = ⋃ (J \times_{t} K)$
49	48	isnei	$⊢ (J \times_{t} K \in Top \land C \times D \subseteq ⋃ (J \times_{t} K)) \to (A \times B \in nei (J \times_{t} K) (C \times D) \leftrightarrow (A \times B \subseteq ⋃ (J \times_{t} K) \land \exists c \in (J \times_{t} K) (C \times D \subseteq c \land c \subseteq A \times B)))$
50	40 47 49	syl2anc	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to (A \times B \in nei (J \times_{t} K) (C \times D) \leftrightarrow (A \times B \subseteq ⋃ (J \times_{t} K) \land \exists c \in (J \times_{t} K) (C \times D \subseteq c \land c \subseteq A \times B)))$
51	11 38 50	mpbir2and	$⊢ ((J \in Top \land K \in Top) \land (A \in nei (J) (C) \land B \in nei (K) (D))) \to A \times B \in nei (J \times_{t} K) (C \times D)$

Metamath Proof Explorer

Theorem neitx

Proof