Theorem txnlly 23704

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 23540	. . 3 ⊢ (𝑅 ∈ 𝑛-Locally 𝐴 → 𝑅 ∈ Top)
2		nllytop 23540	. . 3 ⊢ (𝑆 ∈ 𝑛-Locally 𝐴 → 𝑆 ∈ Top)
3		txtop 23636	. . 3 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑅 ×t 𝑆) ∈ Top)
4	1, 2, 3	syl2an 605	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×t 𝑆) ∈ Top)
5		eltx 23635	. . . 4 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑥 ∈ (𝑅 ×t 𝑆) ↔ ∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥)))
6		simpll 776	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑅 ∈ 𝑛-Locally 𝐴)
7		simprll 788	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑢 ∈ 𝑅)
8		simprrl 790	. . . . . . . . . 10 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑦 ∈ (𝑢 × 𝑣))
9		xp1st 8002	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → (1st ‘𝑦) ∈ 𝑢)
10	8, 9	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (1st ‘𝑦) ∈ 𝑢)
11		nlly2i 23543	. . . . . . . . 9 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑢 ∈ 𝑅 ∧ (1st ‘𝑦) ∈ 𝑢) → ∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴))
12	6, 7, 10, 11	syl3anc 1392	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴))
13		simplr 778	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑆 ∈ 𝑛-Locally 𝐴)
14		simprlr 789	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑣 ∈ 𝑆)
15		xp2nd 8003	. . . . . . . . . 10 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → (2nd ‘𝑦) ∈ 𝑣)
16	8, 15	syl 17	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (2nd ‘𝑦) ∈ 𝑣)
17		nlly2i 23543	. . . . . . . . 9 ⊢ ((𝑆 ∈ 𝑛-Locally 𝐴 ∧ 𝑣 ∈ 𝑆 ∧ (2nd ‘𝑦) ∈ 𝑣) → ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))
18	13, 14, 16, 17	syl3anc 1392	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))
19		reeanv 3235	. . . . . . . . 9 ⊢ (∃𝑎 ∈ 𝒫 𝑢∃𝑏 ∈ 𝒫 𝑣(∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) ↔ (∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)))
20		reeanv 3235	. . . . . . . . . . 11 ⊢ (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) ↔ (∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)))
21	4	ad3antrrr 740	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑅 ×t 𝑆) ∈ Top)
22	1	ad2antrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑅 ∈ Top)
23	22	ad2antrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑅 ∈ Top)
24	13, 2	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → 𝑆 ∈ Top)
25	24	ad2antrr 736	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑆 ∈ Top)
26		simprrl 790	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑟 ∈ 𝑅)
27	26	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑟 ∈ 𝑅)
28		simprrr 791	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑠 ∈ 𝑆)
29	28	adantr 484	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑠 ∈ 𝑆)
30		txopn 23669	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → (𝑟 × 𝑠) ∈ (𝑅 ×t 𝑆))
31	23, 25, 27, 29, 30	syl22anc 849	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ∈ (𝑅 ×t 𝑆))
32	8	ad2antrr 736	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑦 ∈ (𝑢 × 𝑣))
33		1st2nd2 8009	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑦 ∈ (𝑢 × 𝑣) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
34	32, 33	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
35		simprl1 1233	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (1st ‘𝑦) ∈ 𝑟)
36		simprr1 1236	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (2nd ‘𝑦) ∈ 𝑠)
37	35, 36	opelxpd 5687	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ (𝑟 × 𝑠))
38	34, 37	eqeltrd 2863	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑦 ∈ (𝑟 × 𝑠))
39		opnneip 23186	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑅 ×t 𝑆) ∈ Top ∧ (𝑟 × 𝑠) ∈ (𝑅 ×t 𝑆) ∧ 𝑦 ∈ (𝑟 × 𝑠)) → (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×t 𝑆))‘{𝑦}))
40	21, 31, 38, 39	syl3anc 1392	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×t 𝑆))‘{𝑦}))
41		simprl2 1234	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑟 ⊆ 𝑎)
42		simprr2 1237	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑠 ⊆ 𝑏)
43		xpss12 5663	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑟 ⊆ 𝑎 ∧ 𝑠 ⊆ 𝑏) → (𝑟 × 𝑠) ⊆ (𝑎 × 𝑏))
44	41, 42, 43	syl2anc 593	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑟 × 𝑠) ⊆ (𝑎 × 𝑏))
45		simprll 788	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑎 ∈ 𝒫 𝑢)
46	45	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑎 ∈ 𝒫 𝑢)
47	46	elpwid 4565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑎 ⊆ 𝑢)
48	7	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑢 ∈ 𝑅)
49		elssuni 4898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑢 ∈ 𝑅 → 𝑢 ⊆ ∪ 𝑅)
50	48, 49	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑢 ⊆ ∪ 𝑅)
51	47, 50	sstrd 3947	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑎 ⊆ ∪ 𝑅)
52		simprlr 789	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → 𝑏 ∈ 𝒫 𝑣)
53	52	adantr 484	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑏 ∈ 𝒫 𝑣)
54	53	elpwid 4565	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑏 ⊆ 𝑣)
55	14	ad2antrr 736	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑣 ∈ 𝑆)
56		elssuni 4898	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑣 ∈ 𝑆 → 𝑣 ⊆ ∪ 𝑆)
57	55, 56	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑣 ⊆ ∪ 𝑆)
58	54, 57	sstrd 3947	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → 𝑏 ⊆ ∪ 𝑆)
59		xpss12 5663	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ ∪ 𝑅 ∧ 𝑏 ⊆ ∪ 𝑆) → (𝑎 × 𝑏) ⊆ (∪ 𝑅 × ∪ 𝑆))
60	51, 58, 59	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ (∪ 𝑅 × ∪ 𝑆))
61		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑅 = ∪ 𝑅
62		eqid 2763	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∪ 𝑆 = ∪ 𝑆
63	61, 62	txuni 23659	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
64	23, 25, 63	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (∪ 𝑅 × ∪ 𝑆) = ∪ (𝑅 ×t 𝑆))
65	60, 64	sseqtrd 3973	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ ∪ (𝑅 ×t 𝑆))
66		eqid 2763	. . . . . . . . . . . . . . . . . 18 ⊢ ∪ (𝑅 ×t 𝑆) = ∪ (𝑅 ×t 𝑆)
67	66	ssnei2 23183	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑅 ×t 𝑆) ∈ Top ∧ (𝑟 × 𝑠) ∈ ((nei‘(𝑅 ×t 𝑆))‘{𝑦})) ∧ ((𝑟 × 𝑠) ⊆ (𝑎 × 𝑏) ∧ (𝑎 × 𝑏) ⊆ ∪ (𝑅 ×t 𝑆))) → (𝑎 × 𝑏) ∈ ((nei‘(𝑅 ×t 𝑆))‘{𝑦}))
68	21, 40, 44, 65, 67	syl22anc 849	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ ((nei‘(𝑅 ×t 𝑆))‘{𝑦}))
69		xpss12 5663	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑎 ⊆ 𝑢 ∧ 𝑏 ⊆ 𝑣) → (𝑎 × 𝑏) ⊆ (𝑢 × 𝑣))
70	47, 54, 69	syl2anc 593	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ (𝑢 × 𝑣))
71		simprrr 791	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (𝑢 × 𝑣) ⊆ 𝑥)
72	71	ad2antrr 736	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑢 × 𝑣) ⊆ 𝑥)
73	70, 72	sstrd 3947	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ⊆ 𝑥)
74		vex 3459	. . . . . . . . . . . . . . . . . 18 ⊢ 𝑥 ∈ V
75	74	elpw2 5291	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑎 × 𝑏) ∈ 𝒫 𝑥 ↔ (𝑎 × 𝑏) ⊆ 𝑥)
76	73, 75	sylibr 236	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ 𝒫 𝑥)
77	68, 76	elind 4153	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑎 × 𝑏) ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥))
78		txrest 23698	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ∈ Top ∧ 𝑆 ∈ Top) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)) = ((𝑅 ↾t 𝑎) ×t (𝑆 ↾t 𝑏)))
79	23, 25, 46, 53, 78	syl22anc 849	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)) = ((𝑅 ↾t 𝑎) ×t (𝑆 ↾t 𝑏)))
80		simprl3 1235	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑅 ↾t 𝑎) ∈ 𝐴)
81		simprr3 1238	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → (𝑆 ↾t 𝑏) ∈ 𝐴)
82		txlly.1	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴) → (𝑗 ×t 𝑘) ∈ 𝐴)
83	82	caovcl 7590	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑅 ↾t 𝑎) ∈ 𝐴 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴) → ((𝑅 ↾t 𝑎) ×t (𝑆 ↾t 𝑏)) ∈ 𝐴)
84	80, 81, 83	syl2anc 593	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → ((𝑅 ↾t 𝑎) ×t (𝑆 ↾t 𝑏)) ∈ 𝐴)
85	79, 84	eqeltrd 2863	. . . . . . . . . . . . . . 15 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)) ∈ 𝐴)
86		oveq2 7404	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 = (𝑎 × 𝑏) → ((𝑅 ×t 𝑆) ↾t 𝑧) = ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)))
87	86	eleq1d 2848	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 = (𝑎 × 𝑏) → (((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴 ↔ ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)) ∈ 𝐴))
88	87	rspcev 3582	. . . . . . . . . . . . . . 15 ⊢ (((𝑎 × 𝑏) ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥) ∧ ((𝑅 ×t 𝑆) ↾t (𝑎 × 𝑏)) ∈ 𝐴) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴)
89	77, 85, 88	syl2anc 593	. . . . . . . . . . . . . 14 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) ∧ (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴))) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴)
90	89	ex 416	. . . . . . . . . . . . 13 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ ((𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆))) → ((((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
91	90	anassrs 471	. . . . . . . . . . . 12 ⊢ (((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) ∧ (𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆)) → ((((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
92	91	rexlimdvva 3220	. . . . . . . . . . 11 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → (∃𝑟 ∈ 𝑅 ∃𝑠 ∈ 𝑆 (((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
93	20, 92	biimtrrid 245	. . . . . . . . . 10 ⊢ ((((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) ∧ (𝑎 ∈ 𝒫 𝑢 ∧ 𝑏 ∈ 𝒫 𝑣)) → ((∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
94	93	rexlimdvva 3220	. . . . . . . . 9 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → (∃𝑎 ∈ 𝒫 𝑢∃𝑏 ∈ 𝒫 𝑣(∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
95	19, 94	biimtrrid 245	. . . . . . . 8 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ((∃𝑎 ∈ 𝒫 𝑢∃𝑟 ∈ 𝑅 ((1st ‘𝑦) ∈ 𝑟 ∧ 𝑟 ⊆ 𝑎 ∧ (𝑅 ↾t 𝑎) ∈ 𝐴) ∧ ∃𝑏 ∈ 𝒫 𝑣∃𝑠 ∈ 𝑆 ((2nd ‘𝑦) ∈ 𝑠 ∧ 𝑠 ⊆ 𝑏 ∧ (𝑆 ↾t 𝑏) ∈ 𝐴)) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
96	12, 18, 95	mp2and 709	. . . . . . 7 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ ((𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆) ∧ (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥))) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴)
97	96	expr 460	. . . . . 6 ⊢ (((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) ∧ (𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆)) → ((𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
98	97	rexlimdvva 3220	. . . . 5 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
99	98	ralimdv 3177	. . . 4 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (∀𝑦 ∈ 𝑥 ∃𝑢 ∈ 𝑅 ∃𝑣 ∈ 𝑆 (𝑦 ∈ (𝑢 × 𝑣) ∧ (𝑢 × 𝑣) ⊆ 𝑥) → ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
100	5, 99	sylbid 242	. . 3 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑥 ∈ (𝑅 ×t 𝑆) → ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
101	100	ralrimiv 3154	. 2 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → ∀𝑥 ∈ (𝑅 ×t 𝑆)∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴)
102		isnlly 23536	. 2 ⊢ ((𝑅 ×t 𝑆) ∈ 𝑛-Locally 𝐴 ↔ ((𝑅 ×t 𝑆) ∈ Top ∧ ∀𝑥 ∈ (𝑅 ×t 𝑆)∀𝑦 ∈ 𝑥 ∃𝑧 ∈ (((nei‘(𝑅 ×t 𝑆))‘{𝑦}) ∩ 𝒫 𝑥)((𝑅 ×t 𝑆) ↾t 𝑧) ∈ 𝐴))
103	4, 101, 102	sylanbrc 592	1 ⊢ ((𝑅 ∈ 𝑛-Locally 𝐴 ∧ 𝑆 ∈ 𝑛-Locally 𝐴) → (𝑅 ×t 𝑆) ∈ 𝑛-Locally 𝐴)

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1099   = wceq 1561   ∈ wcel 2143  ∀wral 3077  ∃wrex 3087   ∩ cin 3904   ⊆ wss 3905  𝒫 cpw 4556  {csn 4583  ⟨cop 4589  ∪ cuni 4866   × cxp 5646  ‘cfv 6521  (class class class)co 7396  1^st c1st 7968  2^nd c2nd 7969   ↾_t crest 17459  Topctop 22960  neicnei 23164  𝑛-Locally cnlly 23532   ×_t ctx 23627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-rep 5228  ax-sep 5247  ax-nul 5257  ax-pow 5323  ax-pr 5391  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-reu 3369  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-pw 4558  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6477  df-fun 6523  df-fn 6524  df-f 6525  df-f1 6526  df-fo 6527  df-f1o 6528  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971  df-rest 17461  df-topgen 17482  df-top 22961  df-topon 22978  df-bases 23013  df-nei 23165  df-nlly 23534  df-tx 23629

This theorem is referenced by:  xkohmeo  23882  cvmlift2lem13  35670