Theorem neitx 22756

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 22255	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → 𝐴 ⊆ 𝑋)
3	2	ad2ant2r 744	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐴 ⊆ 𝑋)
4		neitx.y	. . . . . 6 ⊢ 𝑌 = ∪ 𝐾
5	4	neii1 22255	. . . . 5 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → 𝐵 ⊆ 𝑌)
6	5	ad2ant2l 743	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐵 ⊆ 𝑌)
7		xpss12 5605	. . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
8	3, 6, 7	syl2anc 584	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
9	1, 4	txuni 22741	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾))
10	9	adantr 481	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾))
11	8, 10	sseqtrd 3966	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ⊆ ∪ (𝐽 ×t 𝐾))
12		simp-5l 782	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
13		simp-4r 781	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑎 ∈ 𝐽)
14		simplr 766	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑏 ∈ 𝐾)
15		txopn 22751	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐾)) → (𝑎 × 𝑏) ∈ (𝐽 ×t 𝐾))
16	12, 13, 14, 15	syl12anc 834	. . . . 5 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝑎 × 𝑏) ∈ (𝐽 ×t 𝐾))
17		simpr1l 1229	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ ((𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴) ∧ 𝑏 ∈ 𝐾 ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))) → 𝐶 ⊆ 𝑎)
18	17	3anassrs 1359	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝐶 ⊆ 𝑎)
19		simprl 768	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝐷 ⊆ 𝑏)
20		xpss12 5605	. . . . . 6 ⊢ ((𝐶 ⊆ 𝑎 ∧ 𝐷 ⊆ 𝑏) → (𝐶 × 𝐷) ⊆ (𝑎 × 𝑏))
21	18, 19, 20	syl2anc 584	. . . . 5 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝐶 × 𝐷) ⊆ (𝑎 × 𝑏))
22		simpr1r 1230	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ ((𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴) ∧ 𝑏 ∈ 𝐾 ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))) → 𝑎 ⊆ 𝐴)
23	22	3anassrs 1359	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑎 ⊆ 𝐴)
24		simprr 770	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑏 ⊆ 𝐵)
25		xpss12 5605	. . . . . 6 ⊢ ((𝑎 ⊆ 𝐴 ∧ 𝑏 ⊆ 𝐵) → (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))
26	23, 24, 25	syl2anc 584	. . . . 5 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))
27		sseq2 3952	. . . . . . 7 ⊢ (𝑐 = (𝑎 × 𝑏) → ((𝐶 × 𝐷) ⊆ 𝑐 ↔ (𝐶 × 𝐷) ⊆ (𝑎 × 𝑏)))
28		sseq1 3951	. . . . . . 7 ⊢ (𝑐 = (𝑎 × 𝑏) → (𝑐 ⊆ (𝐴 × 𝐵) ↔ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵)))
29	27, 28	anbi12d 631	. . . . . 6 ⊢ (𝑐 = (𝑎 × 𝑏) → (((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)) ↔ ((𝐶 × 𝐷) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))))
30	29	rspcev 3561	. . . . 5 ⊢ (((𝑎 × 𝑏) ∈ (𝐽 ×t 𝐾) ∧ ((𝐶 × 𝐷) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
31	16, 21, 26, 30	syl12anc 834	. . . 4 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
32		neii2 22257	. . . . . 6 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
33	32	ad2ant2l 743	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
34	33	ad2antrr 723	. . . 4 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
35	31, 34	r19.29a 3220	. . 3 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
36		neii2 22257	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → ∃𝑎 ∈ 𝐽 (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴))
37	36	ad2ant2r 744	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑎 ∈ 𝐽 (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴))
38	35, 37	r19.29a 3220	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
39		txtop 22718	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ×t 𝐾) ∈ Top)
40	39	adantr 481	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐽 ×t 𝐾) ∈ Top)
41	1	neiss2 22250	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → 𝐶 ⊆ 𝑋)
42	41	ad2ant2r 744	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐶 ⊆ 𝑋)
43	4	neiss2 22250	. . . . . 6 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → 𝐷 ⊆ 𝑌)
44	43	ad2ant2l 743	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐷 ⊆ 𝑌)
45		xpss12 5605	. . . . 5 ⊢ ((𝐶 ⊆ 𝑋 ∧ 𝐷 ⊆ 𝑌) → (𝐶 × 𝐷) ⊆ (𝑋 × 𝑌))
46	42, 44, 45	syl2anc 584	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐶 × 𝐷) ⊆ (𝑋 × 𝑌))
47	46, 10	sseqtrd 3966	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐶 × 𝐷) ⊆ ∪ (𝐽 ×t 𝐾))
48		eqid 2740	. . . 4 ⊢ ∪ (𝐽 ×t 𝐾) = ∪ (𝐽 ×t 𝐾)
49	48	isnei 22252	. . 3 ⊢ (((𝐽 ×t 𝐾) ∈ Top ∧ (𝐶 × 𝐷) ⊆ ∪ (𝐽 ×t 𝐾)) → ((𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)) ↔ ((𝐴 × 𝐵) ⊆ ∪ (𝐽 ×t 𝐾) ∧ ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))))
50	40, 47, 49	syl2anc 584	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ((𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)) ↔ ((𝐴 × 𝐵) ⊆ ∪ (𝐽 ×t 𝐾) ∧ ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))))
51	11, 38, 50	mpbir2and 710	1 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1542   ∈ wcel 2110  ∃wrex 3067   ⊆ wss 3892  ∪ cuni 4845   × cxp 5588  ‘cfv 6432  (class class class)co 7271  Topctop 22040  neicnei 22246   ×_t ctx 22709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7274  df-oprab 7275  df-mpo 7276  df-1st 7824  df-2nd 7825  df-topgen 17152  df-top 22041  df-topon 22058  df-bases 22094  df-nei 22247  df-tx 22711

This theorem is referenced by:  utop2nei  23400  utop3cls  23401