Theorem neitx 15460

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 15339	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → 𝐴 ⊆ 𝑋)
3	2	ad2ant2r 513	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐴 ⊆ 𝑋)
4		neitx.y	. . . . . 6 ⊢ 𝑌 = ∪ 𝐾
5	4	neii1 15339	. . . . 5 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → 𝐵 ⊆ 𝑌)
6	5	ad2ant2l 512	. . . 4 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐵 ⊆ 𝑌)
7		xpss12 4882	. . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝐵 ⊆ 𝑌) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
8	3, 6, 7	syl2anc 415	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐴 × 𝐵) ⊆ (𝑋 × 𝑌))
9	1, 4	txuni 15455	. . . 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 15457	. . . . . 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 4882	. . . . . 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 4882	. . . . . 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 15341	. . . . . 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 15341	. . . 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 15452	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ×t 𝐾) ∈ Top)
40	39	adantr 276	. . 3 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → (𝐽 ×t 𝐾) ∈ Top)
41	1	neiss2 15334	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ ((nei‘𝐽)‘𝐶)) → 𝐶 ⊆ 𝑋)
42	41	ad2ant2r 513	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐶 ⊆ 𝑋)
43	4	neiss2 15334	. . . . . 6 ⊢ ((𝐾 ∈ Top ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷)) → 𝐷 ⊆ 𝑌)
44	43	ad2ant2l 512	. . . . 5 ⊢ (((𝐽 ∈ Top ∧ 𝐾 ∈ Top) ∧ (𝐴 ∈ ((nei‘𝐽)‘𝐶) ∧ 𝐵 ∈ ((nei‘𝐾)‘𝐷))) → 𝐷 ⊆ 𝑌)
45		xpss12 4882	. . . . 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 15336	. . 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 𝐾))‘(𝐶 × 𝐷)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1402   ∈ wcel 2209  ∃wrex 2529   ⊆ wss 3220  ∪ cuni 3935   × cxp 4772  ‘cfv 5377  (class class class)co 6085  Topctop 15189  neicnei 15330   ×_t ctx 15444

This proof depends on 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 4246  ax-sep 4249  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684

This proof 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 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-id 4438  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-ov 6088  df-oprab 6089  df-mpo 6090  df-1st 6374  df-2nd 6375  df-topgen 13667  df-top 15190  df-topon 15203  df-bases 15235  df-nei 15331  df-tx 15445

This theorem is used by: (None)