Theorem neitx 23561

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 23060	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → 𝐴 ⊆ 𝑋)
3	2	ad2ant2r 747	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐴 ⊆ 𝑋)
4		neitx.y	. . . . . 6 ⊢ 𝑌 = ∪ 𝐾
5	4	neii1 23060	. . . . 5 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → 𝐵 ⊆ 𝑌)
6	5	ad2ant2l 746	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐵 ⊆ 𝑌)
7		xpss12 5680	. . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
8	3, 6, 7	syl2anc 584	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
9	1, 4	txuni 23546	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾))
10	9	adantr 480	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾))
11	8, 10	sseqtrd 4000	. 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 23556	. . . . . 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 5680	. . . . . 6 ⊢ ((𝐶 ⊆ 𝑎 ∧ 𝐷 ⊆ 𝑏) → (𝐶 × 𝐷) ⊆ (𝑎 × 𝑏))
21	18, 19, 20	syl2anc 584	. . . . 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 5680	. . . . . 6 ⊢ ((𝑎 ⊆ 𝐴 ∧ 𝑏 ⊆ 𝐵) → (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))
26	23, 24, 25	syl2anc 584	. . . . 5 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))
27		sseq2 3990	. . . . . . 7 ⊢ (𝑐 = (𝑎 × 𝑏) → ((𝐶 × 𝐷) ⊆ 𝑐 ↔ (𝐶 × 𝐷) ⊆ (𝑎 × 𝑏)))
28		sseq1 3989	. . . . . . 7 ⊢ (𝑐 = (𝑎 × 𝑏) → (𝑐 ⊆ (𝐴 × 𝐵) ↔ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵)))
29	27, 28	anbi12d 632	. . . . . 6 ⊢ (𝑐 = (𝑎 × 𝑏) → (((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)) ↔ ((𝐶 × 𝐷) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))))
30	29	rspcev 3605	. . . . 5 ⊢ (((𝑎 × 𝑏) ∈ (𝐽 ×t 𝐾) ∧ ((𝐶 × 𝐷) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
31	16, 21, 26, 30	syl12anc 836	. . . 4 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
32		neii2 23062	. . . . . 6 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
33	32	ad2ant2l 746	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
34	33	ad2antrr 726	. . . 4 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
35	31, 34	r19.29a 3149	. . 3 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
36		neii2 23062	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → ∃𝑎 ∈ 𝐽 (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴))
37	36	ad2ant2r 747	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑎 ∈ 𝐽 (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴))
38	35, 37	r19.29a 3149	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
39		txtop 23523	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ×t 𝐾) ∈ Top)
40	39	adantr 480	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐽 ×t 𝐾) ∈ Top)
41	1	neiss2 23055	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → 𝐶 ⊆ 𝑋)
42	41	ad2ant2r 747	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐶 ⊆ 𝑋)
43	4	neiss2 23055	. . . . . 6 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → 𝐷 ⊆ 𝑌)
44	43	ad2ant2l 746	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐷 ⊆ 𝑌)
45		xpss12 5680	. . . . 5 ⊢ ((𝐶 ⊆ 𝑋 ∧ 𝐷 ⊆ 𝑌) → (𝐶 × 𝐷) ⊆ (𝑋 × 𝑌))
46	42, 44, 45	syl2anc 584	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐶 × 𝐷) ⊆ (𝑋 × 𝑌))
47	46, 10	sseqtrd 4000	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐶 × 𝐷) ⊆ ∪ (𝐽 ×t 𝐾))
48		eqid 2734	. . . 4 ⊢ ∪ (𝐽 ×t 𝐾) = ∪ (𝐽 ×t 𝐾)
49	48	isnei 23057	. . 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 713	1 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  ∃wrex 3059   ⊆ wss 3931  ∪ cuni 4887   × cxp 5663  ‘cfv 6541  (class class class)co 7413  Topctop 22847  neicnei 23051   ×_t ctx 23514

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5259  ax-sep 5276  ax-nul 5286  ax-pow 5345  ax-pr 5412  ax-un 7737

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3420  df-v 3465  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-pw 4582  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4888  df-iun 4973  df-br 5124  df-opab 5186  df-mpt 5206  df-id 5558  df-xp 5671  df-rel 5672  df-cnv 5673  df-co 5674  df-dm 5675  df-rn 5676  df-res 5677  df-ima 5678  df-iota 6494  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7416  df-oprab 7417  df-mpo 7418  df-1st 7996  df-2nd 7997  df-topgen 17459  df-top 22848  df-topon 22865  df-bases 22900  df-nei 23052  df-tx 23516

This theorem is referenced by:  utop2nei  24205  utop3cls  24206