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 23632

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 23468	. . 3 ⊢ (𝑅 ∈ 𝑛-Locally 𝐴 → 𝑅 ∈ Top)
2		nllytop 23468	. . 3 ⊢ (𝑆 ∈ 𝑛-Locally 𝐴 → 𝑆 ∈ Top)
3		txtop 23564	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×_t 𝑆) ∈ Top)
4	1, 2, 3	syl2an 594	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×_t 𝑆) ∈ Top)
5		eltx 23563	. . . 4 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑥 ∈ (𝑅 ×_t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥)))
6		simpll 765	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑅 ∈ 𝑛-Locally 𝐴)
7		simprll 777	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑢 ∈ 𝑅)
8		simprrl 779	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑦 ∈ (𝑢 × 𝑣))
9		xp1st 8035	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → (1^st ‘𝑦) ∈ 𝑢)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (1^st ‘𝑦) ∈ 𝑢)
11		nlly2i 23471	. . . . . . . . 9 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑢 ∈ 𝑅 ∧ (1^st ‘𝑦) ∈ 𝑢) → ∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴))
12	6, 7, 10, 11	syl3anc 1368	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴))
13		simplr 767	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑆 ∈ 𝑛-Locally 𝐴)
14		simprlr 778	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑣 ∈ 𝑆)
15		xp2nd 8036	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → (2^nd ‘𝑦) ∈ 𝑣)
16	8, 15	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (2^nd ‘𝑦) ∈ 𝑣)
17		nlly2i 23471	. . . . . . . . 9 ⊢ ((𝑆 ∈ 𝑛-Locally 𝐴 ∧ 𝑣 ∈ 𝑆 ∧ (2^nd ‘𝑦) ∈ 𝑣) → ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))
18	13, 14, 16, 17	syl3anc 1368	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))
19		reeanv 3217	. . . . . . . . 9 ⊢ (∃𝑎 ∈ 𝒫 𝑢∃𝑏 ∈ 𝒫 𝑣(∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) ↔ (∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)))
20		reeanv 3217	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) ↔ (∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)))
21	4	ad3antrrr 728	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑅 ×_t 𝑆) ∈ Top)
22	1	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑅 ∈ Top)
23	22	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑅 ∈ Top)
24	13, 2	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑆 ∈ Top)
25	24	ad2antrr 724	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑆 ∈ Top)
26		simprrl 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑟 ∈ 𝑅)
27	26	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑟 ∈ 𝑅)
28		simprrr 780	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑠 ∈ 𝑆)
29	28	adantr 479	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑠 ∈ 𝑆)
30		txopn 23597	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 × 𝑠) ∈ (𝑅 ×_t 𝑆))
31	23, 25, 27, 29, 30	syl22anc 837	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ∈ (𝑅 ×_t 𝑆))
32	8	ad2antrr 724	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑦 ∈ (𝑢 × 𝑣))
33		1st2nd2 8042	. . . . . . . . . . . . . . . . . . . 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 1215	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (1^st ‘𝑦) ∈ 𝑟)
36		simprr1 1218	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (2^nd ‘𝑦) ∈ 𝑠)
37	35, 36	opelxpd 5721	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ⟨(1^st ‘𝑦), (2^nd ‘𝑦)⟩ ∈ (𝑟 × 𝑠))
38	34, 37	eqeltrd 2826	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑦 ∈ (𝑟 × 𝑠))
39		opnneip 23114	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ×_t 𝑆) ∈ Top ∧ (𝑟 × 𝑠) ∈ (𝑅 ×_t 𝑆) ∧ 𝑦 ∈ (𝑟 × 𝑠)) → (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
40	21, 31, 38, 39	syl3anc 1368	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
41		simprl2 1216	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑟 ⊆ 𝑎)
42		simprr2 1219	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑠 ⊆ 𝑏)
43		xpss12 5697	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ⊆ 𝑎 ∧ 𝑠 ⊆ 𝑏) → (𝑟 × 𝑠) ⊆ (𝑎 × 𝑏))
44	41, 42, 43	syl2anc 582	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ⊆ (𝑎 × 𝑏))
45		simprll 777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑎 ∈ 𝒫 𝑢)
46	45	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑎 ∈ 𝒫 𝑢)
47	46	elpwid 4616	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑎 ⊆ 𝑢)
48	7	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑢 ∈ 𝑅)
49		elssuni 4945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝑅 → 𝑢 ⊆ ∪ 𝑅)
50	48, 49	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑢 ⊆ ∪ 𝑅)
51	47, 50	sstrd 3990	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑎 ⊆ ∪ 𝑅)
52		simprlr 778	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑏 ∈ 𝒫 𝑣)
53	52	adantr 479	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑏 ∈ 𝒫 𝑣)
54	53	elpwid 4616	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑏 ⊆ 𝑣)
55	14	ad2antrr 724	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑣 ∈ 𝑆)
56		elssuni 4945	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ⊆ ∪ 𝑆)
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑣 ⊆ ∪ 𝑆)
58	54, 57	sstrd 3990	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → 𝑏 ⊆ ∪ 𝑆)
59		xpss12 5697	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ ∪ 𝑅 ∧ 𝑏 ⊆ ∪ 𝑆) → (𝑎 × 𝑏) ⊆ (∪ 𝑅 × ∪ 𝑆))
60	51, 58, 59	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ (∪ 𝑅 × ∪ 𝑆))
61		eqid 2726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑅 = ∪ 𝑅
62		eqid 2726	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑆 = ∪ 𝑆
63	61, 62	txuni 23587	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×_t 𝑆))
64	23, 25, 63	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×_t 𝑆))
65	60, 64	sseqtrd 4020	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ ∪ (𝑅 ×_t 𝑆))
66		eqid 2726	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝑅 ×_t 𝑆) = ∪ (𝑅 ×_t 𝑆)
67	66	ssnei2 23111	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ×_t 𝑆) ∈ Top ∧ (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦})) ∧ ((𝑟 × 𝑠) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ ∪ (𝑅 ×_t 𝑆))) → (𝑎 × 𝑏) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
68	21, 40, 44, 65, 67	syl22anc 837	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ ((nei‘(𝑅 ×_t 𝑆))‘{𝑦}))
69		xpss12 5697	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ 𝑢 ∧ 𝑏 ⊆ 𝑣) → (𝑎 × 𝑏) ⊆ (𝑢 × 𝑣))
70	47, 54, 69	syl2anc 582	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ (𝑢 × 𝑣))
71		simprrr 780	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (𝑢 × 𝑣) ⊆ 𝑥)
72	71	ad2antrr 724	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑢 × 𝑣) ⊆ 𝑥)
73	70, 72	sstrd 3990	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ 𝑥)
74		vex 3466	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
75	74	elpw2 5352	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 × 𝑏) ∈ 𝒫 𝑥 ↔ (𝑎 × 𝑏) ⊆ 𝑥)
76	73, 75	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ 𝒫 𝑥)
77	68, 76	elind 4195	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥))
78		txrest 23626	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) = ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)))
79	23, 25, 46, 53, 78	syl22anc 837	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) = ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)))
80		simprl3 1217	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑅 ↾_t 𝑎) ∈ 𝐴)
81		simprr3 1220	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → (𝑆 ↾_t 𝑏) ∈ 𝐴)
82		txlly.1	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝑗 ×_t 𝑘) ∈ 𝐴)
83	82	caovcl 7620	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ↾_t 𝑎) ∈ 𝐴 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴) → ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)) ∈ 𝐴)
84	80, 81, 83	syl2anc 582	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ((𝑅 ↾_t 𝑎) ×_t (𝑆 ↾_t 𝑏)) ∈ 𝐴)
85	79, 84	eqeltrd 2826	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) ∈ 𝐴)
86		oveq2 7432	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑎 × 𝑏) → ((𝑅 ×_t 𝑆) ↾_t 𝑧) = ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)))
87	86	eleq1d 2811	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑎 × 𝑏) → (((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴 ↔ ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) ∈ 𝐴))
88	87	rspcev 3608	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 × 𝑏) ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝑅 ×_t 𝑆) ↾_t (𝑎 × 𝑏)) ∈ 𝐴) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
89	77, 85, 88	syl2anc 582	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴))) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
90	89	ex 411	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → ((((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
91	90	anassrs 466	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
92	91	rexlimdvva 3202	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
93	20, 92	biimtrrid 242	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → ((∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
94	93	rexlimdvva 3202	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (∃𝑎 ∈ 𝒫 𝑢∃𝑏 ∈ 𝒫 𝑣(∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
95	19, 94	biimtrrid 242	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ((∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1^st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾_t 𝑎) ∈ 𝐴) ∧ ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2^nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾_t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
96	12, 18, 95	mp2and 697	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
97	96	expr 455	. . . . . 6 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ (𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆)) → ((𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
98	97	rexlimdvva 3202	. . . . 5 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
99	98	ralimdv 3159	. . . 4 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
100	5, 99	sylbid 239	. . 3 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑥 ∈ (𝑅 ×_t 𝑆) → ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
101	100	ralrimiv 3135	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → ∀𝑥 ∈ (𝑅 ×_t 𝑆)∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴)
102		isnlly 23464	. 2 ⊢ ((𝑅 ×_t 𝑆) ∈ 𝑛-Locally 𝐴 ↔ ((𝑅 ×_t 𝑆) ∈ Top ∧ ∀𝑥 ∈ (𝑅 ×_t 𝑆)∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×_t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×_t 𝑆) ↾_t 𝑧) ∈ 𝐴))
103	4, 101, 102	sylanbrc 581	1 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×_t 𝑆) ∈ 𝑛-Locally 𝐴)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 394 ∧ w3a 1084 = wceq 1534 ∈ wcel 2099 ∀wral 3051 ∃wrex 3060 ∩ cin 3946 ⊆ wss 3947 𝒫 cpw 4607 {csn 4633 ⟨cop 4639 ∪ cuni 4913 × cxp 5680 ‘cfv 6554 (class class class)co 7424 1^st c1st 8001 2^nd c2nd 8002 ↾_t crest 17435 Topctop 22886 neicnei 23092 𝑛-Locally cnlly 23460 ×_t ctx 23555

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5290 ax-sep 5304 ax-nul 5311 ax-pow 5369 ax-pr 5433 ax-un 7746

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-reu 3365 df-rab 3420 df-v 3464 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4326 df-if 4534 df-pw 4609 df-sn 4634 df-pr 4636 df-op 4640 df-uni 4914 df-iun 5003 df-br 5154 df-opab 5216 df-mpt 5237 df-id 5580 df-xp 5688 df-rel 5689 df-cnv 5690 df-co 5691 df-dm 5692 df-rn 5693 df-res 5694 df-ima 5695 df-iota 6506 df-fun 6556 df-fn 6557 df-f 6558 df-f1 6559 df-fo 6560 df-f1o 6561 df-fv 6562 df-ov 7427 df-oprab 7428 df-mpo 7429 df-1st 8003 df-2nd 8004 df-rest 17437 df-topgen 17458 df-top 22887 df-topon 22904 df-bases 22940 df-nei 23093 df-nlly 23462 df-tx 23557

This theorem is referenced by: xkohmeo 23810 cvmlift2lem13 35143

W3C validator