Theorem txnlly 22786

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 22622	. . 3 ⊢ (𝑅 ∈ 𝑛-Locally 𝐴 → 𝑅 ∈ Top)
2		nllytop 22622	. . 3 ⊢ (𝑆 ∈ 𝑛-Locally 𝐴 → 𝑆 ∈ Top)
3		txtop 22718	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
4	1, 2, 3	syl2an 596	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×t 𝑆) ∈ Top)
5		eltx 22717	. . . 4 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥)))
6		simpll 764	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑅 ∈ 𝑛-Locally 𝐴)
7		simprll 776	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑢 ∈ 𝑅)
8		simprrl 778	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑦 ∈ (𝑢 × 𝑣))
9		xp1st 7856	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → (1st ‘𝑦) ∈ 𝑢)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (1st ‘𝑦) ∈ 𝑢)
11		nlly2i 22625	. . . . . . . . 9 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑢 ∈ 𝑅 ∧ (1st ‘𝑦) ∈ 𝑢) → ∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴))
12	6, 7, 10, 11	syl3anc 1370	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴))
13		simplr 766	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑆 ∈ 𝑛-Locally 𝐴)
14		simprlr 777	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑣 ∈ 𝑆)
15		xp2nd 7857	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → (2nd ‘𝑦) ∈ 𝑣)
16	8, 15	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (2nd ‘𝑦) ∈ 𝑣)
17		nlly2i 22625	. . . . . . . . 9 ⊢ ((𝑆 ∈ 𝑛-Locally 𝐴 ∧ 𝑣 ∈ 𝑆 ∧ (2nd ‘𝑦) ∈ 𝑣) → ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))
18	13, 14, 16, 17	syl3anc 1370	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))
19		reeanv 3295	. . . . . . . . 9 ⊢ (∃𝑎 ∈ 𝒫 𝑢∃𝑏 ∈ 𝒫 𝑣(∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) ↔ (∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)))
20		reeanv 3295	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) ↔ (∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)))
21	4	ad3antrrr 727	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑅 ×t 𝑆) ∈ Top)
22	1	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑅 ∈ Top)
23	22	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑅 ∈ Top)
24	13, 2	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑆 ∈ Top)
25	24	ad2antrr 723	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑆 ∈ Top)
26		simprrl 778	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑟 ∈ 𝑅)
27	26	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑟 ∈ 𝑅)
28		simprrr 779	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑠 ∈ 𝑆)
29	28	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑠 ∈ 𝑆)
30		txopn 22751	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 × 𝑠) ∈ (𝑅 ×t 𝑆))
31	23, 25, 27, 29, 30	syl22anc 836	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ∈ (𝑅 ×t 𝑆))
32	8	ad2antrr 723	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑦 ∈ (𝑢 × 𝑣))
33		1st2nd2 7863	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
35		simprl1 1217	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (1st ‘𝑦) ∈ 𝑟)
36		simprr1 1220	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (2nd ‘𝑦) ∈ 𝑠)
37	35, 36	opelxpd 5628	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ (𝑟 × 𝑠))
38	34, 37	eqeltrd 2841	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑦 ∈ (𝑟 × 𝑠))
39		opnneip 22268	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑟 × 𝑠) ∈ (𝑅 ×t 𝑆) ∧ 𝑦 ∈ (𝑟 × 𝑠)) → (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×t 𝑆))‘{𝑦}))
40	21, 31, 38, 39	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×t 𝑆))‘{𝑦}))
41		simprl2 1218	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑟 ⊆ 𝑎)
42		simprr2 1221	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑠 ⊆ 𝑏)
43		xpss12 5605	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ⊆ 𝑎 ∧ 𝑠 ⊆ 𝑏) → (𝑟 × 𝑠) ⊆ (𝑎 × 𝑏))
44	41, 42, 43	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ⊆ (𝑎 × 𝑏))
45		simprll 776	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑎 ∈ 𝒫 𝑢)
46	45	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑎 ∈ 𝒫 𝑢)
47	46	elpwid 4550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑎 ⊆ 𝑢)
48	7	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑢 ∈ 𝑅)
49		elssuni 4877	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝑅 → 𝑢 ⊆ ∪ 𝑅)
50	48, 49	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑢 ⊆ ∪ 𝑅)
51	47, 50	sstrd 3936	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑎 ⊆ ∪ 𝑅)
52		simprlr 777	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑏 ∈ 𝒫 𝑣)
53	52	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑏 ∈ 𝒫 𝑣)
54	53	elpwid 4550	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑏 ⊆ 𝑣)
55	14	ad2antrr 723	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑣 ∈ 𝑆)
56		elssuni 4877	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ⊆ ∪ 𝑆)
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑣 ⊆ ∪ 𝑆)
58	54, 57	sstrd 3936	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑏 ⊆ ∪ 𝑆)
59		xpss12 5605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ ∪ 𝑅 ∧ 𝑏 ⊆ ∪ 𝑆) → (𝑎 × 𝑏) ⊆ (∪ 𝑅 × ∪ 𝑆))
60	51, 58, 59	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ (∪ 𝑅 × ∪ 𝑆))
61		eqid 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑅 = ∪ 𝑅
62		eqid 2740	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑆 = ∪ 𝑆
63	61, 62	txuni 22741	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
64	23, 25, 63	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
65	60, 64	sseqtrd 3966	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ ∪ (𝑅 ×t 𝑆))
66		eqid 2740	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
67	66	ssnei2 22265	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ×t 𝑆) ∈ Top ∧ (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×t 𝑆))‘{𝑦})) ∧ ((𝑟 × 𝑠) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ ∪ (𝑅 ×t 𝑆))) → (𝑎 × 𝑏) ∈ ((nei‘(𝑅 ×t 𝑆))‘{𝑦}))
68	21, 40, 44, 65, 67	syl22anc 836	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ ((nei‘(𝑅 ×t 𝑆))‘{𝑦}))
69		xpss12 5605	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ 𝑢 ∧ 𝑏 ⊆ 𝑣) → (𝑎 × 𝑏) ⊆ (𝑢 × 𝑣))
70	47, 54, 69	syl2anc 584	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ (𝑢 × 𝑣))
71		simprrr 779	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (𝑢 × 𝑣) ⊆ 𝑥)
72	71	ad2antrr 723	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑢 × 𝑣) ⊆ 𝑥)
73	70, 72	sstrd 3936	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ 𝑥)
74		vex 3435	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
75	74	elpw2 5273	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 × 𝑏) ∈ 𝒫 𝑥 ↔ (𝑎 × 𝑏) ⊆ 𝑥)
76	73, 75	sylibr 233	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ 𝒫 𝑥)
77	68, 76	elind 4133	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥))
78		txrest 22780	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)) = ((𝑅 ↾t 𝑎) ×t (𝑆 ↾t 𝑏)))
79	23, 25, 46, 53, 78	syl22anc 836	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)) = ((𝑅 ↾t 𝑎) ×t (𝑆 ↾t 𝑏)))
80		simprl3 1219	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑅 ↾t 𝑎) ∈ 𝐴)
81		simprr3 1222	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑆 ↾t 𝑏) ∈ 𝐴)
82		txlly.1	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝑗 ×t 𝑘) ∈ 𝐴)
83	82	caovcl 7460	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ↾t 𝑎) ∈ 𝐴 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴) → ((𝑅 ↾t 𝑎) ×t (𝑆 ↾t 𝑏)) ∈ 𝐴)
84	80, 81, 83	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → ((𝑅 ↾t 𝑎) ×t (𝑆 ↾t 𝑏)) ∈ 𝐴)
85	79, 84	eqeltrd 2841	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)) ∈ 𝐴)
86		oveq2 7279	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑎 × 𝑏) → ((𝑅 ×t 𝑆) ↾t 𝑧) = ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)))
87	86	eleq1d 2825	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑎 × 𝑏) → (((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴 ↔ ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)) ∈ 𝐴))
88	87	rspcev 3561	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 × 𝑏) ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)) ∈ 𝐴) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴)
89	77, 85, 88	syl2anc 584	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴)
90	89	ex 413	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → ((((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
91	90	anassrs 468	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
92	91	rexlimdvva 3225	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
93	20, 92	syl5bir 242	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → ((∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
94	93	rexlimdvva 3225	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (∃𝑎 ∈ 𝒫 𝑢∃𝑏 ∈ 𝒫 𝑣(∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
95	19, 94	syl5bir 242	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ((∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
96	12, 18, 95	mp2and 696	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴)
97	96	expr 457	. . . . . 6 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ (𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆)) → ((𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
98	97	rexlimdvva 3225	. . . . 5 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
99	98	ralimdv 3106	. . . 4 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
100	5, 99	sylbid 239	. . 3 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑥 ∈ (𝑅 ×t 𝑆) → ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
101	100	ralrimiv 3109	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → ∀𝑥 ∈ (𝑅 ×t 𝑆)∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴)
102		isnlly 22618	. 2 ⊢ ((𝑅 ×t 𝑆) ∈ 𝑛-Locally 𝐴 ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ∀𝑥 ∈ (𝑅 ×t 𝑆)∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
103	4, 101, 102	sylanbrc 583	1 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×t 𝑆) ∈ 𝑛-Locally 𝐴)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086   = wceq 1542   ∈ wcel 2110  ∀wral 3066  ∃wrex 3067   ∩ cin 3891   ⊆ wss 3892  𝒫 cpw 4539  {csn 4567  ⟨cop 4573  ∪ cuni 4845   × cxp 5588  ‘cfv 6432  (class class class)co 7271  1^st c1st 7822  2^nd c2nd 7823   ↾_t crest 17129  Topctop 22040  neicnei 22246  𝑛-Locally cnlly 22614   ×_t ctx 22709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2711  ax-rep 5214  ax-sep 5227  ax-nul 5234  ax-pow 5292  ax-pr 5356  ax-un 7582

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2072  df-mo 2542  df-eu 2571  df-clab 2718  df-cleq 2732  df-clel 2818  df-nfc 2891  df-ne 2946  df-ral 3071  df-rex 3072  df-reu 3073  df-rab 3075  df-v 3433  df-sbc 3721  df-csb 3838  df-dif 3895  df-un 3897  df-in 3899  df-ss 3909  df-nul 4263  df-if 4466  df-pw 4541  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4846  df-iun 4932  df-br 5080  df-opab 5142  df-mpt 5163  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6390  df-fun 6434  df-fn 6435  df-f 6436  df-f1 6437  df-fo 6438  df-f1o 6439  df-fv 6440  df-ov 7274  df-oprab 7275  df-mpo 7276  df-1st 7824  df-2nd 7825  df-rest 17131  df-topgen 17152  df-top 22041  df-topon 22058  df-bases 22094  df-nei 22247  df-nlly 22616  df-tx 22711

This theorem is referenced by:  xkohmeo  22964  cvmlift2lem13  33273