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 23666

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 23502	. . 3 ⊢ (𝑅 ∈ 𝑛-Locally 𝐴 → 𝑅 ∈ Top)
2		nllytop 23502	. . 3 ⊢ (𝑆 ∈ 𝑛-Locally 𝐴 → 𝑆 ∈ Top)
3		txtop 23598	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×_t 𝑆) ∈ Top)
4	1, 2, 3	syl2an 604	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×_t 𝑆) ∈ Top)
5		eltx 23597	. . . 4 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑥 ∈ (𝑅 ×_t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥)))
6		simpll 774	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑅 ∈ 𝑛-Locally 𝐴)
7		simprll 786	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑢 ∈ 𝑅)
8		simprrl 788	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑦 ∈ (𝑢 × 𝑣))
9		xp1st 7987	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → (1^st ‘𝑦) ∈ 𝑢)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (1^st ‘𝑦) ∈ 𝑢)
11		nlly2i 23505	. . . . . . . . 9 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑢 ∈ 𝑅 ∧ (1^st ‘𝑦) ∈ 𝑢) → ∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴))
12	6, 7, 10, 11	syl3anc 1382	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴))
13		simplr 776	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑆 ∈ 𝑛-Locally 𝐴)
14		simprlr 787	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑣 ∈ 𝑆)
15		xp2nd 7988	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → (2^nd ‘𝑦) ∈ 𝑣)
16	8, 15	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (2^nd ‘𝑦) ∈ 𝑣)
17		nlly2i 23505	. . . . . . . . 9 ⊢ ((𝑆 ∈ 𝑛-Locally 𝐴 ∧ 𝑣 ∈ 𝑆 ∧ (2^nd ‘𝑦) ∈ 𝑣) → ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))
18	13, 14, 16, 17	syl3anc 1382	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))
19		reeanv 3224	. . . . . . . . 9 ⊢ (∃𝑎 ∈ 𝒫 𝑢∃𝑏 ∈ 𝒫 𝑣(∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) ↔ (∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)))
20		reeanv 3224	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) ↔ (∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)))
21	4	ad3antrrr 738	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑅 ×_t 𝑆) ∈ Top)
22	1	ad2antrr 734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑅 ∈ Top)
23	22	ad2antrr 734	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑅 ∈ Top)
24	13, 2	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑆 ∈ Top)
25	24	ad2antrr 734	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑆 ∈ Top)
26		simprrl 788	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑟 ∈ 𝑅)
27	26	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑟 ∈ 𝑅)
28		simprrr 789	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑠 ∈ 𝑆)
29	28	adantr 483	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑠 ∈ 𝑆)
30		txopn 23631	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 × 𝑠) ∈ (𝑅 ×_t 𝑆))
31	23, 25, 27, 29, 30	syl22anc 847	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ∈ (𝑅 ×_t 𝑆))
32	8	ad2antrr 734	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑦 ∈ (𝑢 × 𝑣))
33		1st2nd2 7994	. . . . . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (1^st ‘𝑦) ∈ 𝑟)
36		simprr1 1231	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (2^nd ‘𝑦) ∈ 𝑠)
37	35, 36	opelxpd 5675	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝑟 × 𝑠))
38	34, 37	eqeltrd 2852	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑦 ∈ (𝑟 × 𝑠))
39		opnneip 23148	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ×_t 𝑆) ∈ Top ∧ (𝑟 × 𝑠) ∈ (𝑅 ×_t 𝑆) ∧ 𝑦 ∈ (𝑟 × 𝑠)) → (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
40	21, 31, 38, 39	syl3anc 1382	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
41		simprl2 1229	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑟 ⊆ 𝑎)
42		simprr2 1232	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑠 ⊆ 𝑏)
43		xpss12 5651	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ⊆ 𝑎 ∧ 𝑠 ⊆ 𝑏) → (𝑟 × 𝑠) ⊆ (𝑎 × 𝑏))
44	41, 42, 43	syl2anc 592	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ⊆ (𝑎 × 𝑏))
45		simprll 786	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑎 ∈ 𝒫 𝑢)
46	45	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑎 ∈ 𝒫 𝑢)
47	46	elpwid 4554	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑎 ⊆ 𝑢)
48	7	ad2antrr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑢 ∈ 𝑅)
49		elssuni 4887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝑅 → 𝑢 ⊆ ∪ 𝑅)
50	48, 49	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑢 ⊆ ∪ 𝑅)
51	47, 50	sstrd 3937	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑎 ⊆ ∪ 𝑅)
52		simprlr 787	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑏 ∈ 𝒫 𝑣)
53	52	adantr 483	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑏 ∈ 𝒫 𝑣)
54	53	elpwid 4554	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑏 ⊆ 𝑣)
55	14	ad2antrr 734	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑣 ∈ 𝑆)
56		elssuni 4887	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ⊆ ∪ 𝑆)
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑣 ⊆ ∪ 𝑆)
58	54, 57	sstrd 3937	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑏 ⊆ ∪ 𝑆)
59		xpss12 5651	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ ∪ 𝑅 ∧ 𝑏 ⊆ ∪ 𝑆) → (𝑎 × 𝑏) ⊆ (∪ 𝑅 × ∪ 𝑆))
60	51, 58, 59	syl2anc 592	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ (∪ 𝑅 × ∪ 𝑆))
61		eqid 2752	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑅 = ∪ 𝑅
62		eqid 2752	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑆 = ∪ 𝑆
63	61, 62	txuni 23621	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×_t 𝑆))
64	23, 25, 63	syl2anc 592	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×_t 𝑆))
65	60, 64	sseqtrd 3963	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ ∪ (𝑅 ×_t 𝑆))
66		eqid 2752	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝑅 ×_t 𝑆) = ∪ (𝑅 ×_t 𝑆)
67	66	ssnei2 23145	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ×_t 𝑆) ∈ Top ∧ (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦})) ∧ ((𝑟 × 𝑠) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ ∪ (𝑅 ×_t 𝑆))) → (𝑎 × 𝑏) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
68	21, 40, 44, 65, 67	syl22anc 847	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
69		xpss12 5651	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ 𝑢 ∧ 𝑏 ⊆ 𝑣) → (𝑎 × 𝑏) ⊆ (𝑢 × 𝑣))
70	47, 54, 69	syl2anc 592	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ (𝑢 × 𝑣))
71		simprrr 789	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (𝑢 × 𝑣) ⊆ 𝑥)
72	71	ad2antrr 734	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑢 × 𝑣) ⊆ 𝑥)
73	70, 72	sstrd 3937	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ 𝑥)
74		vex 3448	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
75	74	elpw2 5280	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 × 𝑏) ∈ 𝒫 𝑥 ↔ (𝑎 × 𝑏) ⊆ 𝑥)
76	73, 75	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ 𝒫 𝑥)
77	68, 76	elind 4143	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥))
78		txrest 23660	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) = ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)))
79	23, 25, 46, 53, 78	syl22anc 847	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) = ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)))
80		simprl3 1230	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑅 ↾_t 𝑎) ∈ 𝐴)
81		simprr3 1233	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑆 ↾_t 𝑏) ∈ 𝐴)
82		txlly.1	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝑗 ×_t 𝑘) ∈ 𝐴)
83	82	caovcl 7575	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ↾_t 𝑎) ∈ 𝐴 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴) → ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)) ∈ 𝐴)
84	80, 81, 83	syl2anc 592	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)) ∈ 𝐴)
85	79, 84	eqeltrd 2852	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) ∈ 𝐴)
86		oveq2 7389	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑎 × 𝑏) → ((𝑅 ×_t 𝑆) ↾_t 𝑧) = ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)))
87	86	eleq1d 2837	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑎 × 𝑏) → (((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴 ↔ ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) ∈ 𝐴))
88	87	rspcev 3572	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 × 𝑏) ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) ∈ 𝐴) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
89	77, 85, 88	syl2anc 592	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
90	89	ex 415	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → ((((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
91	90	anassrs 470	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
92	91	rexlimdvva 3209	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
93	20, 92	biimtrrid 245	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → ((∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
94	93	rexlimdvva 3209	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (∃𝑎 ∈ 𝒫 𝑢∃𝑏 ∈ 𝒫 𝑣(∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
95	19, 94	biimtrrid 245	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ((∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
96	12, 18, 95	mp2and 707	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
97	96	expr 459	. . . . . 6 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ (𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆)) → ((𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
98	97	rexlimdvva 3209	. . . . 5 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
99	98	ralimdv 3166	. . . 4 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
100	5, 99	sylbid 242	. . 3 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑥 ∈ (𝑅 ×_t 𝑆) → ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
101	100	ralrimiv 3143	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → ∀𝑥 ∈ (𝑅 ×_t 𝑆)∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
102		isnlly 23498	. 2 ⊢ ((𝑅 ×_t 𝑆) ∈ 𝑛-Locally 𝐴 ↔ ((𝑅 ×_t 𝑆) ∈ Top ∧ ∀𝑥 ∈ (𝑅 ×_t 𝑆)∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
103	4, 101, 102	sylanbrc 591	1 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×_t 𝑆) ∈ 𝑛-Locally 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1095 = wceq 1550 ∈ wcel 2132 ∀wral 3066 ∃wrex 3076 ∩ cin 3894 ⊆ wss 3895 𝒫 cpw 4545 {csn 4572 ⟨cop 4578 ∪ cuni 4855 × cxp 5634 ‘cfv 6506 (class class class)co 7381 1^st c1st 7953 2^nd c2nd 7954 ↾_t crest 17421 Topctop 22922 neicnei 23126 𝑛-Locally cnlly 23494 ×_t ctx 23589

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1805 ax-4 1819 ax-5 1920 ax-6 1977 ax-7 2018 ax-8 2134 ax-9 2142 ax-10 2165 ax-11 2181 ax-12 2202 ax-ext 2724 ax-rep 5217 ax-sep 5236 ax-nul 5246 ax-pow 5312 ax-pr 5380 ax-un 7703

This theorem depends on definitions: df-bi 209 df-an 399 df-or 857 df-3an 1097 df-tru 1553 df-fal 1563 df-ex 1790 df-nf 1794 df-sb 2081 df-mo 2556 df-eu 2586 df-clab 2731 df-cleq 2744 df-clel 2827 df-nfc 2901 df-ne 2948 df-ral 3067 df-rex 3077 df-reu 3358 df-rab 3405 df-v 3446 df-sbc 3736 df-csb 3844 df-dif 3898 df-un 3900 df-in 3902 df-ss 3912 df-nul 4277 df-if 4471 df-pw 4547 df-sn 4573 df-pr 4575 df-op 4579 df-uni 4856 df-iun 4941 df-br 5091 df-opab 5153 df-mpt 5172 df-id 5531 df-xp 5642 df-rel 5643 df-cnv 5644 df-co 5645 df-dm 5646 df-rn 5647 df-res 5648 df-ima 5649 df-iota 6462 df-fun 6508 df-fn 6509 df-f 6510 df-f1 6511 df-fo 6512 df-f1o 6513 df-fv 6514 df-ov 7384 df-oprab 7385 df-mpo 7386 df-1st 7955 df-2nd 7956 df-rest 17423 df-topgen 17444 df-top 22923 df-topon 22940 df-bases 22975 df-nei 23127 df-nlly 23496 df-tx 23591

This theorem is referenced by: xkohmeo 23844 cvmlift2lem13 35603

W3C validator