Theorem neitx 15292

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 15171	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → 𝐴 ⊆ 𝑋)
3	2	ad2ant2r 513	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐴 ⊆ 𝑋)
4		neitx.y	. . . . . 6 ⊢ 𝑌 = ∪ 𝐾
5	4	neii1 15171	. . . . 5 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → 𝐵 ⊆ 𝑌)
6	5	ad2ant2l 512	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐵 ⊆ 𝑌)
7		xpss12 4877	. . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
8	3, 6, 7	syl2anc 415	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
9	1, 4	txuni 15287	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾))
10	9	adantr 276	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝑋 × 𝑌) = ∪ (𝐽 ×t 𝐾))
11	8, 10	sseqtrd 3286	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ⊆ ∪ (𝐽 ×t 𝐾))
12		simp-5l 549	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝐽 ∈ Top ∧ 𝐾 ∈ Top))
13		simp-4r 548	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑎 ∈ 𝐽)
14		simplr 533	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑏 ∈ 𝐾)
15		txopn 15289	. . . . . 6 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝑎 ∈ 𝐽 ∧ 𝑏 ∈ 𝐾)) → (𝑎 × 𝑏) ∈ (𝐽 ×t 𝐾))
16	12, 13, 14, 15	syl12anc 1276	. . . . 5 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝑎 × 𝑏) ∈ (𝐽 ×t 𝐾))
17		simpr1l 1085	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ ((𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴) ∧ 𝑏 ∈ 𝐾 ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))) → 𝐶 ⊆ 𝑎)
18	17	3anassrs 1260	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝐶 ⊆ 𝑎)
19		simprl 535	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝐷 ⊆ 𝑏)
20		xpss12 4877	. . . . . 6 ⊢ ((𝐶 ⊆ 𝑎 ∧ 𝐷 ⊆ 𝑏) → (𝐶 × 𝐷) ⊆ (𝑎 × 𝑏))
21	18, 19, 20	syl2anc 415	. . . . 5 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝐶 × 𝐷) ⊆ (𝑎 × 𝑏))
22		simpr1r 1086	. . . . . . 7 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ ((𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴) ∧ 𝑏 ∈ 𝐾 ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))) → 𝑎 ⊆ 𝐴)
23	22	3anassrs 1260	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑎 ⊆ 𝐴)
24		simprr 537	. . . . . 6 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → 𝑏 ⊆ 𝐵)
25		xpss12 4877	. . . . . 6 ⊢ ((𝑎 ⊆ 𝐴 ∧ 𝑏 ⊆ 𝐵) → (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))
26	23, 24, 25	syl2anc 415	. . . . 5 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))
27		sseq2 3272	. . . . . . 7 ⊢ (𝑐 = (𝑎 × 𝑏) → ((𝐶 × 𝐷) ⊆ 𝑐 ↔ (𝐶 × 𝐷) ⊆ (𝑎 × 𝑏)))
28		sseq1 3271	. . . . . . 7 ⊢ (𝑐 = (𝑎 × 𝑏) → (𝑐 ⊆ (𝐴 × 𝐵) ↔ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵)))
29	27, 28	anbi12d 477	. . . . . 6 ⊢ (𝑐 = (𝑎 × 𝑏) → (((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)) ↔ ((𝐶 × 𝐷) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))))
30	29	rspcev 2929	. . . . 5 ⊢ (((𝑎 × 𝑏) ∈ (𝐽 ×t 𝐾) ∧ ((𝐶 × 𝐷) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ (𝐴 × 𝐵))) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
31	16, 21, 26, 30	syl12anc 1276	. . . 4 ⊢ (((((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) ∧ 𝑏 ∈ 𝐾) ∧ (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵)) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
32		neii2 15173	. . . . . 6 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
33	32	ad2ant2l 512	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
34	33	ad2antrr 492	. . . 4 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) → ∃𝑏 ∈ 𝐾 (𝐷 ⊆ 𝑏 ∧ 𝑏 ⊆ 𝐵))
35	31, 34	r19.29a 2694	. . 3 ⊢ (((((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) ∧ 𝑎 ∈ 𝐽) ∧ (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴)) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
36		neii2 15173	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → ∃𝑎 ∈ 𝐽 (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴))
37	36	ad2ant2r 513	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑎 ∈ 𝐽 (𝐶 ⊆ 𝑎 ∧ 𝑎 ⊆ 𝐴))
38	35, 37	r19.29a 2694	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))
39		txtop 15284	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ×t 𝐾) ∈ Top)
40	39	adantr 276	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐽 ×t 𝐾) ∈ Top)
41	1	neiss2 15166	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → 𝐶 ⊆ 𝑋)
42	41	ad2ant2r 513	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐶 ⊆ 𝑋)
43	4	neiss2 15166	. . . . . 6 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → 𝐷 ⊆ 𝑌)
44	43	ad2ant2l 512	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐷 ⊆ 𝑌)
45		xpss12 4877	. . . . 5 ⊢ ((𝐶 ⊆ 𝑋 ∧ 𝐷 ⊆ 𝑌) → (𝐶 × 𝐷) ⊆ (𝑋 × 𝑌))
46	42, 44, 45	syl2anc 415	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐶 × 𝐷) ⊆ (𝑋 × 𝑌))
47	46, 10	sseqtrd 3286	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐶 × 𝐷) ⊆ ∪ (𝐽 ×t 𝐾))
48		eqid 2238	. . . 4 ⊢ ∪ (𝐽 ×t 𝐾) = ∪ (𝐽 ×t 𝐾)
49	48	isnei 15168	. . 3 ⊢ (((𝐽 ×t 𝐾) ∈ Top ∧ (𝐶 × 𝐷) ⊆ ∪ (𝐽 ×t 𝐾)) → ((𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)) ↔ ((𝐴 × 𝐵) ⊆ ∪ (𝐽 ×t 𝐾) ∧ ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))))
50	40, 47, 49	syl2anc 415	. 2 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → ((𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)) ↔ ((𝐴 × 𝐵) ⊆ ∪ (𝐽 ×t 𝐾) ∧ ∃𝑐 ∈ (𝐽 ×t 𝐾)((𝐶 × 𝐷) ⊆ 𝑐 ∧ 𝑐 ⊆ (𝐴 × 𝐵)))))
51	11, 38, 50	mpbir2and 957	1 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ∈ ((nei‘(𝐽 ×t 𝐾))‘(𝐶 × 𝐷)))

Syntax hints:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∃wrex 2529   ⊆ wss 3220  ∪ cuni 3930   × cxp 4767  ‘cfv 5372  (class class class)co 6075  Topctop 15021  neicnei 15162   ×_t ctx 15276

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4241  ax-sep 4244  ax-pow 4306  ax-pr 4341  ax-un 4573  ax-setind 4679

This theorem depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-pw 3687  df-sn 3711  df-pr 3712  df-op 3714  df-uni 3931  df-iun 4009  df-br 4126  df-opab 4188  df-mpt 4189  df-id 4433  df-xp 4775  df-rel 4776  df-cnv 4777  df-co 4778  df-dm 4779  df-rn 4780  df-res 4781  df-ima 4782  df-iota 5332  df-fun 5374  df-fn 5375  df-f 5376  df-f1 5377  df-fo 5378  df-f1o 5379  df-fv 5380  df-ov 6078  df-oprab 6079  df-mpo 6080  df-1st 6364  df-2nd 6365  df-topgen 13591  df-top 15022  df-topon 15035  df-bases 15067  df-nei 15163  df-tx 15277

This theorem is referenced by: (None)