Metamath Proof Explorer


Theorem neitx

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

Ref Expression
Hypotheses neitx.x 𝑋 = 𝐽
neitx.y 𝑌 = 𝐾
Assertion neitx ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ( 𝐴 × 𝐵 ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐾 ) ) ‘ ( 𝐶 × 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 neitx.x 𝑋 = 𝐽
2 neitx.y 𝑌 = 𝐾
3 1 neii1 ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ) → 𝐴𝑋 )
4 3 ad2ant2r ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → 𝐴𝑋 )
5 2 neii1 ( ( 𝐾 ∈ Top ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) → 𝐵𝑌 )
6 5 ad2ant2l ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → 𝐵𝑌 )
7 xpss12 ( ( 𝐴𝑋𝐵𝑌 ) → ( 𝐴 × 𝐵 ) ⊆ ( 𝑋 × 𝑌 ) )
8 4 6 7 syl2anc ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ( 𝐴 × 𝐵 ) ⊆ ( 𝑋 × 𝑌 ) )
9 1 2 txuni ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝑋 × 𝑌 ) = ( 𝐽 ×t 𝐾 ) )
10 9 adantr ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ( 𝑋 × 𝑌 ) = ( 𝐽 ×t 𝐾 ) )
11 8 10 sseqtrd ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ( 𝐴 × 𝐵 ) ⊆ ( 𝐽 ×t 𝐾 ) )
12 simp-5l ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) ∧ 𝑏𝐾 ) ∧ ( 𝐷𝑏𝑏𝐵 ) ) → ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) )
13 simp-4r ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) ∧ 𝑏𝐾 ) ∧ ( 𝐷𝑏𝑏𝐵 ) ) → 𝑎𝐽 )
14 simplr ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) ∧ 𝑏𝐾 ) ∧ ( 𝐷𝑏𝑏𝐵 ) ) → 𝑏𝐾 )
15 txopn ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝑎𝐽𝑏𝐾 ) ) → ( 𝑎 × 𝑏 ) ∈ ( 𝐽 ×t 𝐾 ) )
16 12 13 14 15 syl12anc ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) ∧ 𝑏𝐾 ) ∧ ( 𝐷𝑏𝑏𝐵 ) ) → ( 𝑎 × 𝑏 ) ∈ ( 𝐽 ×t 𝐾 ) )
17 simpr1l ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( ( 𝐶𝑎𝑎𝐴 ) ∧ 𝑏𝐾 ∧ ( 𝐷𝑏𝑏𝐵 ) ) ) → 𝐶𝑎 )
18 17 3anassrs ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) ∧ 𝑏𝐾 ) ∧ ( 𝐷𝑏𝑏𝐵 ) ) → 𝐶𝑎 )
19 simprl ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) ∧ 𝑏𝐾 ) ∧ ( 𝐷𝑏𝑏𝐵 ) ) → 𝐷𝑏 )
20 xpss12 ( ( 𝐶𝑎𝐷𝑏 ) → ( 𝐶 × 𝐷 ) ⊆ ( 𝑎 × 𝑏 ) )
21 18 19 20 syl2anc ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) ∧ 𝑏𝐾 ) ∧ ( 𝐷𝑏𝑏𝐵 ) ) → ( 𝐶 × 𝐷 ) ⊆ ( 𝑎 × 𝑏 ) )
22 simpr1r ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( ( 𝐶𝑎𝑎𝐴 ) ∧ 𝑏𝐾 ∧ ( 𝐷𝑏𝑏𝐵 ) ) ) → 𝑎𝐴 )
23 22 3anassrs ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) ∧ 𝑏𝐾 ) ∧ ( 𝐷𝑏𝑏𝐵 ) ) → 𝑎𝐴 )
24 simprr ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) ∧ 𝑏𝐾 ) ∧ ( 𝐷𝑏𝑏𝐵 ) ) → 𝑏𝐵 )
25 xpss12 ( ( 𝑎𝐴𝑏𝐵 ) → ( 𝑎 × 𝑏 ) ⊆ ( 𝐴 × 𝐵 ) )
26 23 24 25 syl2anc ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) ∧ 𝑏𝐾 ) ∧ ( 𝐷𝑏𝑏𝐵 ) ) → ( 𝑎 × 𝑏 ) ⊆ ( 𝐴 × 𝐵 ) )
27 sseq2 ( 𝑐 = ( 𝑎 × 𝑏 ) → ( ( 𝐶 × 𝐷 ) ⊆ 𝑐 ↔ ( 𝐶 × 𝐷 ) ⊆ ( 𝑎 × 𝑏 ) ) )
28 sseq1 ( 𝑐 = ( 𝑎 × 𝑏 ) → ( 𝑐 ⊆ ( 𝐴 × 𝐵 ) ↔ ( 𝑎 × 𝑏 ) ⊆ ( 𝐴 × 𝐵 ) ) )
29 27 28 anbi12d ( 𝑐 = ( 𝑎 × 𝑏 ) → ( ( ( 𝐶 × 𝐷 ) ⊆ 𝑐𝑐 ⊆ ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝐶 × 𝐷 ) ⊆ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐴 × 𝐵 ) ) ) )
30 29 rspcev ( ( ( 𝑎 × 𝑏 ) ∈ ( 𝐽 ×t 𝐾 ) ∧ ( ( 𝐶 × 𝐷 ) ⊆ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ( 𝐴 × 𝐵 ) ) ) → ∃ 𝑐 ∈ ( 𝐽 ×t 𝐾 ) ( ( 𝐶 × 𝐷 ) ⊆ 𝑐𝑐 ⊆ ( 𝐴 × 𝐵 ) ) )
31 16 21 26 30 syl12anc ( ( ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) ∧ 𝑏𝐾 ) ∧ ( 𝐷𝑏𝑏𝐵 ) ) → ∃ 𝑐 ∈ ( 𝐽 ×t 𝐾 ) ( ( 𝐶 × 𝐷 ) ⊆ 𝑐𝑐 ⊆ ( 𝐴 × 𝐵 ) ) )
32 neii2 ( ( 𝐾 ∈ Top ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) → ∃ 𝑏𝐾 ( 𝐷𝑏𝑏𝐵 ) )
33 32 ad2ant2l ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ∃ 𝑏𝐾 ( 𝐷𝑏𝑏𝐵 ) )
34 33 ad2antrr ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) → ∃ 𝑏𝐾 ( 𝐷𝑏𝑏𝐵 ) )
35 31 34 r19.29a ( ( ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) ∧ 𝑎𝐽 ) ∧ ( 𝐶𝑎𝑎𝐴 ) ) → ∃ 𝑐 ∈ ( 𝐽 ×t 𝐾 ) ( ( 𝐶 × 𝐷 ) ⊆ 𝑐𝑐 ⊆ ( 𝐴 × 𝐵 ) ) )
36 neii2 ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ) → ∃ 𝑎𝐽 ( 𝐶𝑎𝑎𝐴 ) )
37 36 ad2ant2r ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ∃ 𝑎𝐽 ( 𝐶𝑎𝑎𝐴 ) )
38 35 37 r19.29a ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ∃ 𝑐 ∈ ( 𝐽 ×t 𝐾 ) ( ( 𝐶 × 𝐷 ) ⊆ 𝑐𝑐 ⊆ ( 𝐴 × 𝐵 ) ) )
39 txtop ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) → ( 𝐽 ×t 𝐾 ) ∈ Top )
40 39 adantr ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ( 𝐽 ×t 𝐾 ) ∈ Top )
41 1 neiss2 ( ( 𝐽 ∈ Top ∧ 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ) → 𝐶𝑋 )
42 41 ad2ant2r ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → 𝐶𝑋 )
43 2 neiss2 ( ( 𝐾 ∈ Top ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) → 𝐷𝑌 )
44 43 ad2ant2l ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → 𝐷𝑌 )
45 xpss12 ( ( 𝐶𝑋𝐷𝑌 ) → ( 𝐶 × 𝐷 ) ⊆ ( 𝑋 × 𝑌 ) )
46 42 44 45 syl2anc ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ( 𝐶 × 𝐷 ) ⊆ ( 𝑋 × 𝑌 ) )
47 46 10 sseqtrd ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ( 𝐶 × 𝐷 ) ⊆ ( 𝐽 ×t 𝐾 ) )
48 eqid ( 𝐽 ×t 𝐾 ) = ( 𝐽 ×t 𝐾 )
49 48 isnei ( ( ( 𝐽 ×t 𝐾 ) ∈ Top ∧ ( 𝐶 × 𝐷 ) ⊆ ( 𝐽 ×t 𝐾 ) ) → ( ( 𝐴 × 𝐵 ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐾 ) ) ‘ ( 𝐶 × 𝐷 ) ) ↔ ( ( 𝐴 × 𝐵 ) ⊆ ( 𝐽 ×t 𝐾 ) ∧ ∃ 𝑐 ∈ ( 𝐽 ×t 𝐾 ) ( ( 𝐶 × 𝐷 ) ⊆ 𝑐𝑐 ⊆ ( 𝐴 × 𝐵 ) ) ) ) )
50 40 47 49 syl2anc ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ( ( 𝐴 × 𝐵 ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐾 ) ) ‘ ( 𝐶 × 𝐷 ) ) ↔ ( ( 𝐴 × 𝐵 ) ⊆ ( 𝐽 ×t 𝐾 ) ∧ ∃ 𝑐 ∈ ( 𝐽 ×t 𝐾 ) ( ( 𝐶 × 𝐷 ) ⊆ 𝑐𝑐 ⊆ ( 𝐴 × 𝐵 ) ) ) ) )
51 11 38 50 mpbir2and ( ( ( 𝐽 ∈ Top ∧ 𝐾 ∈ Top ) ∧ ( 𝐴 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐶 ) ∧ 𝐵 ∈ ( ( nei ‘ 𝐾 ) ‘ 𝐷 ) ) ) → ( 𝐴 × 𝐵 ) ∈ ( ( nei ‘ ( 𝐽 ×t 𝐾 ) ) ‘ ( 𝐶 × 𝐷 ) ) )