txnlly - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > txnlly		Structured version Visualization version GIF version

Theorem txnlly 21440

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

**Hypothesis**
Ref	Expression
txlly.1	⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝑗 ×_t 𝑘) ∈ 𝐴)

**Assertion**
Ref	Expression
txnlly	⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×_t 𝑆) ∈ 𝑛-Locally 𝐴)

Distinct variable groups: 𝑗,𝑘,𝐴 𝑅,𝑗,𝑘 𝑆,𝑘 Allowed substitution hint: 𝑆(𝑗)

Proof of Theorem txnlly Dummy variables 𝑎 𝑏 𝑟 𝑠 𝑢 𝑣 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nllytop 21276	. . 3 ⊢ (𝑅 ∈ 𝑛-Locally 𝐴 → 𝑅 ∈ Top)
2		nllytop 21276	. . 3 ⊢ (𝑆 ∈ 𝑛-Locally 𝐴 → 𝑆 ∈ Top)
3		txtop 21372	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×_t 𝑆) ∈ Top)
4	1, 2, 3	syl2an 494	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×_t 𝑆) ∈ Top)
5		eltx 21371	. . . 4 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑥 ∈ (𝑅 ×_t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥)))
6		simpll 790	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑅 ∈ 𝑛-Locally 𝐴)
7		simprll 802	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑢 ∈ 𝑅)
8		simprrl 804	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑦 ∈ (𝑢 × 𝑣))
9		xp1st 7198	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → (1^st ‘𝑦) ∈ 𝑢)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (1^st ‘𝑦) ∈ 𝑢)
11		nlly2i 21279	. . . . . . . . 9 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑢 ∈ 𝑅 ∧ (1^st ‘𝑦) ∈ 𝑢) → ∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴))
12	6, 7, 10, 11	syl3anc 1326	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴))
13		simplr 792	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑆 ∈ 𝑛-Locally 𝐴)
14		simprlr 803	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑣 ∈ 𝑆)
15		xp2nd 7199	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → (2^nd ‘𝑦) ∈ 𝑣)
16	8, 15	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (2^nd ‘𝑦) ∈ 𝑣)
17		nlly2i 21279	. . . . . . . . 9 ⊢ ((𝑆 ∈ 𝑛-Locally 𝐴 ∧ 𝑣 ∈ 𝑆 ∧ (2^nd ‘𝑦) ∈ 𝑣) → ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))
18	13, 14, 16, 17	syl3anc 1326	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))
19		reeanv 3107	. . . . . . . . 9 ⊢ (∃𝑎 ∈ 𝒫 𝑢∃𝑏 ∈ 𝒫 𝑣(∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) ↔ (∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)))
20		reeanv 3107	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) ↔ (∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)))
21	4	ad3antrrr 766	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑅 ×_t 𝑆) ∈ Top)
22	1	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑅 ∈ Top)
23	22	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑅 ∈ Top)
24	13, 2	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑆 ∈ Top)
25	24	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑆 ∈ Top)
26		simprrl 804	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑟 ∈ 𝑅)
27	26	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑟 ∈ 𝑅)
28		simprrr 805	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑠 ∈ 𝑆)
29	28	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑠 ∈ 𝑆)
30		txopn 21405	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 × 𝑠) ∈ (𝑅 ×_t 𝑆))
31	23, 25, 27, 29, 30	syl22anc 1327	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ∈ (𝑅 ×_t 𝑆))
32	8	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑦 ∈ (𝑢 × 𝑣))
33		1st2nd2 7205	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑦 = ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩)
35		simprl1 1106	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (1^st ‘𝑦) ∈ 𝑟)
36		simprr1 1109	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (2^nd ‘𝑦) ∈ 𝑠)
37		opelxpi 5148	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((1^st ‘𝑦) ∈ 𝑟 ∧ (2^nd ‘𝑦) ∈ 𝑠) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝑟 × 𝑠))
38	35, 36, 37	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝑟 × 𝑠))
39	34, 38	eqeltrd 2701	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑦 ∈ (𝑟 × 𝑠))
40		opnneip 20923	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ×_t 𝑆) ∈ Top ∧ (𝑟 × 𝑠) ∈ (𝑅 ×_t 𝑆) ∧ 𝑦 ∈ (𝑟 × 𝑠)) → (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
41	21, 31, 39, 40	syl3anc 1326	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
42		simprl2 1107	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑟 ⊆ 𝑎)
43		simprr2 1110	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑠 ⊆ 𝑏)
44		xpss12 5225	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ⊆ 𝑎 ∧ 𝑠 ⊆ 𝑏) → (𝑟 × 𝑠) ⊆ (𝑎 × 𝑏))
45	42, 43, 44	syl2anc 693	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ⊆ (𝑎 × 𝑏))
46		simprll 802	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑎 ∈ 𝒫 𝑢)
47	46	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑎 ∈ 𝒫 𝑢)
48	47	elpwid 4170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑎 ⊆ 𝑢)
49	7	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑢 ∈ 𝑅)
50		elssuni 4467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝑅 → 𝑢 ⊆ ∪ 𝑅)
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑢 ⊆ ∪ 𝑅)
52	48, 51	sstrd 3613	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑎 ⊆ ∪ 𝑅)
53		simprlr 803	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑏 ∈ 𝒫 𝑣)
54	53	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑏 ∈ 𝒫 𝑣)
55	54	elpwid 4170	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑏 ⊆ 𝑣)
56	14	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑣 ∈ 𝑆)
57		elssuni 4467	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ⊆ ∪ 𝑆)
58	56, 57	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑣 ⊆ ∪ 𝑆)
59	55, 58	sstrd 3613	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑏 ⊆ ∪ 𝑆)
60		xpss12 5225	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ ∪ 𝑅 ∧ 𝑏 ⊆ ∪ 𝑆) → (𝑎 × 𝑏) ⊆ (∪ 𝑅 × ∪ 𝑆))
61	52, 59, 60	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ (∪ 𝑅 × ∪ 𝑆))
62		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑅 = ∪ 𝑅
63		eqid 2622	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑆 = ∪ 𝑆
64	62, 63	txuni 21395	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×_t 𝑆))
65	23, 25, 64	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×_t 𝑆))
66	61, 65	sseqtrd 3641	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ ∪ (𝑅 ×_t 𝑆))
67		eqid 2622	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝑅 ×_t 𝑆) = ∪ (𝑅 ×_t 𝑆)
68	67	ssnei2 20920	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ×_t 𝑆) ∈ Top ∧ (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦})) ∧ ((𝑟 × 𝑠) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ ∪ (𝑅 ×_t 𝑆))) → (𝑎 × 𝑏) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
69	21, 41, 45, 66, 68	syl22anc 1327	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
70		xpss12 5225	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ 𝑢 ∧ 𝑏 ⊆ 𝑣) → (𝑎 × 𝑏) ⊆ (𝑢 × 𝑣))
71	48, 55, 70	syl2anc 693	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ (𝑢 × 𝑣))
72		simprrr 805	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (𝑢 × 𝑣) ⊆ 𝑥)
73	72	ad2antrr 762	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑢 × 𝑣) ⊆ 𝑥)
74	71, 73	sstrd 3613	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ 𝑥)
75		vex 3203	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
76	75	elpw2 4828	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 × 𝑏) ∈ 𝒫 𝑥 ↔ (𝑎 × 𝑏) ⊆ 𝑥)
77	74, 76	sylibr 224	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ 𝒫 𝑥)
78	69, 77	elind 3798	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥))
79		txrest 21434	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) = ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)))
80	23, 25, 47, 54, 79	syl22anc 1327	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) = ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)))
81		simprl3 1108	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑅 ↾_t 𝑎) ∈ 𝐴)
82		simprr3 1111	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑆 ↾_t 𝑏) ∈ 𝐴)
83		txlly.1	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝑗 ×_t 𝑘) ∈ 𝐴)
84	83	caovcl 6828	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ↾_t 𝑎) ∈ 𝐴 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴) → ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)) ∈ 𝐴)
85	81, 82, 84	syl2anc 693	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)) ∈ 𝐴)
86	80, 85	eqeltrd 2701	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) ∈ 𝐴)
87		oveq2 6658	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑎 × 𝑏) → ((𝑅 ×_t 𝑆) ↾_t 𝑧) = ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)))
88	87	eleq1d 2686	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑎 × 𝑏) → (((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴 ↔ ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) ∈ 𝐴))
89	88	rspcev 3309	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 × 𝑏) ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) ∈ 𝐴) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
90	78, 86, 89	syl2anc 693	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
91	90	ex 450	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → ((((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
92	91	anassrs 680	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
93	92	rexlimdvva 3038	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
94	20, 93	syl5bir 233	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → ((∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
95	94	rexlimdvva 3038	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (∃𝑎 ∈ 𝒫 𝑢∃𝑏 ∈ 𝒫 𝑣(∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
96	19, 95	syl5bir 233	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ((∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
97	12, 18, 96	mp2and 715	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
98	97	expr 643	. . . . . 6 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ (𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆)) → ((𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
99	98	rexlimdvva 3038	. . . . 5 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
100	99	ralimdv 2963	. . . 4 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
101	5, 100	sylbid 230	. . 3 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑥 ∈ (𝑅 ×_t 𝑆) → ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
102	101	ralrimiv 2965	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → ∀𝑥 ∈ (𝑅 ×_t 𝑆)∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
103		isnlly 21272	. 2 ⊢ ((𝑅 ×_t 𝑆) ∈ 𝑛-Locally 𝐴 ↔ ((𝑅 ×_t 𝑆) ∈ Top ∧ ∀𝑥 ∈ (𝑅 ×_t 𝑆)∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
104	4, 102, 103	sylanbrc 698	1 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×_t 𝑆) ∈ 𝑛-Locally 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 384 ∧ w3a 1037 = wceq 1483 ∈ wcel 1990 ∀wral 2912 ∃wrex 2913 ∩ cin 3573 ⊆ wss 3574 𝒫 cpw 4158 {csn 4177 ⟨cop 4183 ∪ cuni 4436 × cxp 5112 ‘cfv 5888 (class class class)co 6650 1^st c1st 7166 2^nd c2nd 7167 ↾_t crest 16081 Topctop 20698 neicnei 20901 𝑛-Locally cnlly 21268 ×_t ctx 21363

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3an 1039 df-tru 1486 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-ral 2917 df-rex 2918 df-reu 2919 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-op 4184 df-uni 4437 df-iun 4522 df-br 4654 df-opab 4713 df-mpt 4730 df-id 5024 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-1st 7168 df-2nd 7169 df-rest 16083 df-topgen 16104 df-top 20699 df-topon 20716 df-bases 20750 df-nei 20902 df-nlly 21270 df-tx 21365

This theorem is referenced by: xkohmeo 21618 cvmlift2lem13 31297

W3C validator