This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐾 ) ) ‘ ( 𝐶 × 𝐷 ) ) )