Metamath Proof Explorer

Theorem txnlly

Description: If the property A is preserved under topological products, then so is the property of being n-locally A . (Contributed by Mario Carneiro, 13-Apr-2015)

Ref Expression
Hypothesis txlly.1 ⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑗 ×t 𝑘 ) ∈ 𝐴 )
Assertion txnlly ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) → ( 𝑅 ×t 𝑆 ) ∈ 𝑛-Locally 𝐴 )

Proof

Step Hyp Ref Expression
1 txlly.1 ⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑗 ×t 𝑘 ) ∈ 𝐴 )
2 nllytop ⊢ ( 𝑅 ∈ 𝑛-Locally 𝐴 → 𝑅 ∈ Top )
3 nllytop ⊢ ( 𝑆 ∈ 𝑛-Locally 𝐴 → 𝑆 ∈ Top )
4 txtop ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
5 2 3 4 syl2an ⊢ ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
6 eltx ⊢ ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) → ( 𝑥 ∈ ( 𝑅 ×t 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) )
7 simpll ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑅 ∈ 𝑛-Locally 𝐴 )
8 simprll ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑢 ∈ 𝑅 )
9 simprrl ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑦 ∈ ( 𝑢 × 𝑣 ) )
10 xp1st ⊢ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) → ( 1st ‘ 𝑦 ) ∈ 𝑢 )
11 9 10 syl ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( 1st ‘ 𝑦 ) ∈ 𝑢 )
12 nlly2i ⊢ ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑢 ∈ 𝑅 ∧ ( 1st ‘ 𝑦 ) ∈ 𝑢 ) → ∃ 𝑎 ∈ 𝒫 𝑢 ∃ 𝑟 ∈ 𝑅 ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) )
13 7 8 11 12 syl3anc ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ∃ 𝑎 ∈ 𝒫 𝑢 ∃ 𝑟 ∈ 𝑅 ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) )
14 simplr ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑆 ∈ 𝑛-Locally 𝐴 )
15 simprlr ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑣 ∈ 𝑆 )
16 xp2nd ⊢ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) → ( 2nd ‘ 𝑦 ) ∈ 𝑣 )
17 9 16 syl ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( 2nd ‘ 𝑦 ) ∈ 𝑣 )
18 nlly2i ⊢ ( ( 𝑆 ∈ 𝑛-Locally 𝐴 ∧ 𝑣 ∈ 𝑆 ∧ ( 2nd ‘ 𝑦 ) ∈ 𝑣 ) → ∃ 𝑏 ∈ 𝒫 𝑣 ∃ 𝑠 ∈ 𝑆 ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) )
19 14 15 17 18 syl3anc ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ∃ 𝑏 ∈ 𝒫 𝑣 ∃ 𝑠 ∈ 𝑆 ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) )
20 reeanv ⊢ ( ∃ 𝑎 ∈ 𝒫 𝑢 ∃ 𝑏 ∈ 𝒫 𝑣 ( ∃ 𝑟 ∈ 𝑅 ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑆 ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ↔ ( ∃ 𝑎 ∈ 𝒫 𝑢 ∃ 𝑟 ∈ 𝑅 ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ∃ 𝑏 ∈ 𝒫 𝑣 ∃ 𝑠 ∈ 𝑆 ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) )
21 reeanv ⊢ ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ↔ ( ∃ 𝑟 ∈ 𝑅 ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑆 ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) )
22 5 ad3antrrr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑅 ×t 𝑆 ) ∈ Top )
23 2 ad2antrr ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑅 ∈ Top )
24 23 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑅 ∈ Top )
25 14 3 syl ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑆 ∈ Top )
26 25 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑆 ∈ Top )
27 simprrl ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) → 𝑟 ∈ 𝑅 )
28 27 adantr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑟 ∈ 𝑅 )
29 simprrr ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) → 𝑠 ∈ 𝑆 )
30 29 adantr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑠 ∈ 𝑆 )
31 txopn ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝑟 × 𝑠 ) ∈ ( 𝑅 ×t 𝑆 ) )
32 24 26 28 30 31 syl22anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑟 × 𝑠 ) ∈ ( 𝑅 ×t 𝑆 ) )
33 9 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑦 ∈ ( 𝑢 × 𝑣 ) )
34 1st2nd2 ⊢ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) → 𝑦 = ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ )
35 33 34 syl ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑦 = ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ )
36 simprl1 ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 1st ‘ 𝑦 ) ∈ 𝑟 )
37 simprr1 ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 2nd ‘ 𝑦 ) ∈ 𝑠 )
38 36 37 opelxpd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ⟨ ( 1st ‘ 𝑦 ) , ( 2nd ‘ 𝑦 ) ⟩ ∈ ( 𝑟 × 𝑠 ) )
39 35 38 eqeltrd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑦 ∈ ( 𝑟 × 𝑠 ) )
40 opnneip ⊢ ( ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ( 𝑟 × 𝑠 ) ∈ ( 𝑅 ×t 𝑆 ) ∧ 𝑦 ∈ ( 𝑟 × 𝑠 ) ) → ( 𝑟 × 𝑠 ) ∈ ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) )
41 22 32 39 40 syl3anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑟 × 𝑠 ) ∈ ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) )
42 simprl2 ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑟 ⊆ 𝑎 )
43 simprr2 ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑠 ⊆ 𝑏 )
44 xpss12 ⊢ ( ( 𝑟 ⊆ 𝑎 ∧ 𝑠 ⊆ 𝑏 ) → ( 𝑟 × 𝑠 ) ⊆ ( 𝑎 × 𝑏 ) )
45 42 43 44 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑟 × 𝑠 ) ⊆ ( 𝑎 × 𝑏 ) )
46 simprll ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) → 𝑎 ∈ 𝒫 𝑢 )
47 46 adantr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑎 ∈ 𝒫 𝑢 )
48 47 elpwid ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑎 ⊆ 𝑢 )
49 8 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑢 ∈ 𝑅 )
50 elssuni ⊢ ( 𝑢 ∈ 𝑅 → 𝑢 ⊆ ∪ 𝑅 )
51 49 50 syl ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑢 ⊆ ∪ 𝑅 )
52 48 51 sstrd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑎 ⊆ ∪ 𝑅 )
53 simprlr ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) → 𝑏 ∈ 𝒫 𝑣 )
54 53 adantr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑏 ∈ 𝒫 𝑣 )
55 54 elpwid ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑏 ⊆ 𝑣 )
56 15 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑣 ∈ 𝑆 )
57 elssuni ⊢ ( 𝑣 ∈ 𝑆 → 𝑣 ⊆ ∪ 𝑆 )
58 56 57 syl ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑣 ⊆ ∪ 𝑆 )
59 55 58 sstrd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → 𝑏 ⊆ ∪ 𝑆 )
60 xpss12 ⊢ ( ( 𝑎 ⊆ ∪ 𝑅 ∧ 𝑏 ⊆ ∪ 𝑆 ) → ( 𝑎 × 𝑏 ) ⊆ ( ∪ 𝑅 × ∪ 𝑆 ) )
61 52 59 60 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑎 × 𝑏 ) ⊆ ( ∪ 𝑅 × ∪ 𝑆 ) )
62 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
63 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
64 62 63 txuni ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) )
65 24 26 64 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( ∪ 𝑅 × ∪ 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 ) )
66 61 65 sseqtrd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑎 × 𝑏 ) ⊆ ∪ ( 𝑅 ×t 𝑆 ) )
67 eqid ⊢ ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 )
68 67 ssnei2 ⊢ ( ( ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ( 𝑟 × 𝑠 ) ∈ ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ) ∧ ( ( 𝑟 × 𝑠 ) ⊆ ( 𝑎 × 𝑏 ) ∧ ( 𝑎 × 𝑏 ) ⊆ ∪ ( 𝑅 ×t 𝑆 ) ) ) → ( 𝑎 × 𝑏 ) ∈ ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) )
69 22 41 45 66 68 syl22anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑎 × 𝑏 ) ∈ ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) )
70 xpss12 ⊢ ( ( 𝑎 ⊆ 𝑢 ∧ 𝑏 ⊆ 𝑣 ) → ( 𝑎 × 𝑏 ) ⊆ ( 𝑢 × 𝑣 ) )
71 48 55 70 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑎 × 𝑏 ) ⊆ ( 𝑢 × 𝑣 ) )
72 simprrr ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( 𝑢 × 𝑣 ) ⊆ 𝑥 )
73 72 ad2antrr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑢 × 𝑣 ) ⊆ 𝑥 )
74 71 73 sstrd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑎 × 𝑏 ) ⊆ 𝑥 )
75 vex ⊢ 𝑥 ∈ V
76 75 elpw2 ⊢ ( ( 𝑎 × 𝑏 ) ∈ 𝒫 𝑥 ↔ ( 𝑎 × 𝑏 ) ⊆ 𝑥 )
77 74 76 sylibr ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑎 × 𝑏 ) ∈ 𝒫 𝑥 )
78 69 77 elind ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑎 × 𝑏 ) ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) )
79 txrest ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑎 × 𝑏 ) ) = ( ( 𝑅 ↾t 𝑎 ) ×t ( 𝑆 ↾t 𝑏 ) ) )
80 24 26 47 54 79 syl22anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑎 × 𝑏 ) ) = ( ( 𝑅 ↾t 𝑎 ) ×t ( 𝑆 ↾t 𝑏 ) ) )
81 simprl3 ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 )
82 simprr3 ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 )
83 1 caovcl ⊢ ( ( ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) → ( ( 𝑅 ↾t 𝑎 ) ×t ( 𝑆 ↾t 𝑏 ) ) ∈ 𝐴 )
84 81 82 83 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( ( 𝑅 ↾t 𝑎 ) ×t ( 𝑆 ↾t 𝑏 ) ) ∈ 𝐴 )
85 80 84 eqeltrd ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑎 × 𝑏 ) ) ∈ 𝐴 )
86 oveq2 ⊢ ( 𝑧 = ( 𝑎 × 𝑏 ) → ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) = ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑎 × 𝑏 ) ) )
87 86 eleq1d ⊢ ( 𝑧 = ( 𝑎 × 𝑏 ) → ( ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ↔ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑎 × 𝑏 ) ) ∈ 𝐴 ) )
88 87 rspcev ⊢ ( ( ( 𝑎 × 𝑏 ) ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ∧ ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑎 × 𝑏 ) ) ∈ 𝐴 ) → ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 )
89 78 85 88 syl2anc ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) ∧ ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) ) → ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 )
90 89 ex ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ) → ( ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
91 90 anassrs ⊢ ( ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
92 91 rexlimdvva ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ) → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
93 21 92 biimtrrid ⊢ ( ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣 ) ) → ( ( ∃ 𝑟 ∈ 𝑅 ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑆 ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
94 93 rexlimdvva ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( ∃ 𝑎 ∈ 𝒫 𝑢 ∃ 𝑏 ∈ 𝒫 𝑣 ( ∃ 𝑟 ∈ 𝑅 ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑆 ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
95 20 94 biimtrrid ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( ( ∃ 𝑎 ∈ 𝒫 𝑢 ∃ 𝑟 ∈ 𝑅 ( ( 1st ‘ 𝑦 ) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ ( 𝑅 ↾t 𝑎 ) ∈ 𝐴 ) ∧ ∃ 𝑏 ∈ 𝒫 𝑣 ∃ 𝑠 ∈ 𝑆 ( ( 2nd ‘ 𝑦 ) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ ( 𝑆 ↾t 𝑏 ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
96 13 19 95 mp2and ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 )
97 96 expr ⊢ ( ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) ∧ ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) → ( ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) → ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
98 97 rexlimdvva ⊢ ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) → ( ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) → ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
99 98 ralimdv ⊢ ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
100 6 99 sylbid ⊢ ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) → ( 𝑥 ∈ ( 𝑅 ×t 𝑆 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
101 100 ralrimiv ⊢ ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) → ∀ 𝑥 ∈ ( 𝑅 ×t 𝑆 ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 )
102 isnlly ⊢ ( ( 𝑅 ×t 𝑆 ) ∈ 𝑛-Locally 𝐴 ↔ ( ( 𝑅 ×t 𝑆 ) ∈ Top ∧ ∀ 𝑥 ∈ ( 𝑅 ×t 𝑆 ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( ( ( nei ‘ ( 𝑅 ×t 𝑆 ) ) ‘ { 𝑦 } ) ∩ 𝒫 𝑥 ) ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
103 5 101 102 sylanbrc ⊢ ( ( 𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴 ) → ( 𝑅 ×t 𝑆 ) ∈ 𝑛-Locally 𝐴 )