Theorem neitx 23629

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

Hypotheses

Ref	Expression
neitx.x	⊢ 𝑋 = ∪ 𝐽
neitx.y	⊢ 𝑌 = ∪ 𝐾

Assertion

Ref	Expression
neitx	⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)))

Proof of Theorem neitx

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		neitx.x	. . . . . 6 ⊢ 𝑋 = ∪ 𝐽
2	1	neii1 23128	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → 𝐴 ⊆ 𝑋)
3	2	ad2ant2r 746	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐴 ⊆ 𝑋)
4		neitx.y	. . . . . 6 ⊢ 𝑌 = ∪ 𝐾
5	4	neii1 23128	. . . . 5 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → 𝐵 ⊆ 𝑌)
6	5	ad2ant2l 745	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐵 ⊆ 𝑌)
7		xpss12 5714	. . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
8	3, 6, 7	syl2anc 583	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
9	1, 4	txuni 23614	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾))
10	9	adantr 480	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾))
11	8, 10	sseqtrd 4043	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ⊆ ∪ (𝐽 ×t 𝐾))
12		simp-5l 784	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
13		simp-4r 783	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑎 ∈ 𝐽)
14		simplr 768	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑏 ∈ 𝐾)
15		txopn 23624	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐾)) → (𝑎 × 𝑏) ∈ (𝐽 ×t 𝐾))
16	12, 13, 14, 15	syl12anc 836	. . . . 5 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝑎 × 𝑏) ∈ (𝐽 ×t 𝐾))
17		simpr1l 1230	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ ((𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴) ∧ 𝑏 ∈ 𝐾 ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))) → 𝐶 ⊆ 𝑎)
18	17	3anassrs 1360	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝐶 ⊆ 𝑎)
19		simprl 770	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝐷 ⊆ 𝑏)
20		xpss12 5714	. . . . . 6 ⊢ ((𝐶 ⊆ 𝑎 ∧ 𝐷 ⊆ 𝑏) → (𝐶 × 𝐷) ⊆ (𝑎 × 𝑏))
21	18, 19, 20	syl2anc 583	. . . . 5 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝐶 × 𝐷) ⊆ (𝑎 × 𝑏))
22		simpr1r 1231	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ ((𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴) ∧ 𝑏 ∈ 𝐾 ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))) → 𝑎 ⊆ 𝐴)
23	22	3anassrs 1360	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑎 ⊆ 𝐴)
24		simprr 772	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑏 ⊆ 𝐵)
25		xpss12 5714	. . . . . 6 ⊢ ((𝑎 ⊆ 𝐴 ∧ 𝑏 ⊆ 𝐵) → (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))
26	23, 24, 25	syl2anc 583	. . . . 5 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))
27		sseq2 4029	. . . . . . 7 ⊢ (𝑐 = (𝑎 × 𝑏) → ((𝐶 × 𝐷) ⊆ 𝑐 ↔ (𝐶 × 𝐷) ⊆ (𝑎 × 𝑏)))
28		sseq1 4028	. . . . . . 7 ⊢ (𝑐 = (𝑎 × 𝑏) → (𝑐 ⊆ (𝐴 × 𝐵) ↔ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵)))
29	27, 28	anbi12d 631	. . . . . 6 ⊢ (𝑐 = (𝑎 × 𝑏) → (((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)) ↔ ((𝐶 × 𝐷) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))))
30	29	rspcev 3631	. . . . 5 ⊢ (((𝑎 × 𝑏) ∈ (𝐽 ×t 𝐾) ∧ ((𝐶 × 𝐷) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
31	16, 21, 26, 30	syl12anc 836	. . . 4 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
32		neii2 23130	. . . . . 6 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
33	32	ad2ant2l 745	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
34	33	ad2antrr 725	. . . 4 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
35	31, 34	r19.29a 3164	. . 3 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
36		neii2 23130	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → ∃𝑎 ∈ 𝐽 (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴))
37	36	ad2ant2r 746	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑎 ∈ 𝐽 (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴))
38	35, 37	r19.29a 3164	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
39		txtop 23591	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ×t 𝐾) ∈ Top)
40	39	adantr 480	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐽 ×t 𝐾) ∈ Top)
41	1	neiss2 23123	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → 𝐶 ⊆ 𝑋)
42	41	ad2ant2r 746	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐶 ⊆ 𝑋)
43	4	neiss2 23123	. . . . . 6 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → 𝐷 ⊆ 𝑌)
44	43	ad2ant2l 745	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐷 ⊆ 𝑌)
45		xpss12 5714	. . . . 5 ⊢ ((𝐶 ⊆ 𝑋 ∧ 𝐷 ⊆ 𝑌) → (𝐶 × 𝐷) ⊆ (𝑋 × 𝑌))
46	42, 44, 45	syl2anc 583	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐶 × 𝐷) ⊆ (𝑋 × 𝑌))
47	46, 10	sseqtrd 4043	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐶 × 𝐷) ⊆ ∪ (𝐽 ×t 𝐾))
48		eqid 2734	. . . 4 ⊢ ∪ (𝐽 ×t 𝐾) = ∪ (𝐽 ×t 𝐾)
49	48	isnei 23125	. . 3 ⊢ (((𝐽 ×t 𝐾) ∈ Top ∧ (𝐶 × 𝐷) ⊆ ∪ (𝐽 ×t 𝐾)) → ((𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)) ↔ ((𝐴 × 𝐵) ⊆ ∪ (𝐽 ×t 𝐾) ∧ ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))))
50	40, 47, 49	syl2anc 583	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ((𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)) ↔ ((𝐴 × 𝐵) ⊆ ∪ (𝐽 ×t 𝐾) ∧ ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))))
51	11, 38, 50	mpbir2and 712	1 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1537   ∈ wcel 2103  ∃wrex 3072   ⊆ wss 3970  ∪ cuni 4931   × cxp 5697  ‘cfv 6572  (class class class)co 7445  Topctop 22913  neicnei 23119   ×_t ctx 23582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2105  ax-9 2113  ax-10 2136  ax-11 2153  ax-12 2173  ax-ext 2705  ax-rep 5306  ax-sep 5320  ax-nul 5327  ax-pow 5386  ax-pr 5450  ax-un 7766

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-nf 1782  df-sb 2065  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2890  df-ne 2943  df-ral 3064  df-rex 3073  df-reu 3384  df-rab 3439  df-v 3484  df-sbc 3799  df-csb 3916  df-dif 3973  df-un 3975  df-in 3977  df-ss 3987  df-nul 4348  df-if 4549  df-pw 4624  df-sn 4649  df-pr 4651  df-op 4655  df-uni 4932  df-iun 5021  df-br 5170  df-opab 5232  df-mpt 5253  df-id 5597  df-xp 5705  df-rel 5706  df-cnv 5707  df-co 5708  df-dm 5709  df-rn 5710  df-res 5711  df-ima 5712  df-iota 6524  df-fun 6574  df-fn 6575  df-f 6576  df-f1 6577  df-fo 6578  df-f1o 6579  df-fv 6580  df-ov 7448  df-oprab 7449  df-mpo 7450  df-1st 8026  df-2nd 8027  df-topgen 17498  df-top 22914  df-topon 22931  df-bases 22967  df-nei 23120  df-tx 23584

This theorem is referenced by:  utop2nei  24273  utop3cls  24274