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