txlly

Description: If the property A is preserved under topological products, then so is the property of being locally A . (Contributed by Mario Carneiro, 10-Mar-2015)

		Ref	Expression
	Hypothesis	txlly.1	⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑗 ×_t 𝑘 ) ∈ 𝐴 )
	Assertion	txlly	⊢ ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) → ( 𝑅 ×_t 𝑆 ) ∈ Locally 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		txlly.1	⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐴 ) → ( 𝑗 ×_t 𝑘 ) ∈ 𝐴 )
2		llytop	⊢ ( 𝑅 ∈ Locally 𝐴 → 𝑅 ∈ Top )
3		llytop	⊢ ( 𝑆 ∈ Locally 𝐴 → 𝑆 ∈ Top )
4		txtop	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×_t 𝑆 ) ∈ Top )
5	2 3 4	syl2an	⊢ ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) → ( 𝑅 ×_t 𝑆 ) ∈ Top )
6		eltx	⊢ ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) → ( 𝑥 ∈ ( 𝑅 ×_t 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) )
7		simpll	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑅 ∈ Locally 𝐴 )
8		simprll	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑢 ∈ 𝑅 )
9		simprrl	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑦 ∈ ( 𝑢 × 𝑣 ) )
10		xp1st	⊢ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) → ( 1^st ‘ 𝑦 ) ∈ 𝑢 )
11	9 10	syl	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( 1^st ‘ 𝑦 ) ∈ 𝑢 )
12		llyi	⊢ ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑢 ∈ 𝑅 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑢 ) → ∃ 𝑟 ∈ 𝑅 ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) )
13	7 8 11 12	syl3anc	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ∃ 𝑟 ∈ 𝑅 ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) )
14		simplr	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑆 ∈ Locally 𝐴 )
15		simprlr	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑣 ∈ 𝑆 )
16		xp2nd	⊢ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) → ( 2^nd ‘ 𝑦 ) ∈ 𝑣 )
17	9 16	syl	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( 2^nd ‘ 𝑦 ) ∈ 𝑣 )
18		llyi	⊢ ( ( 𝑆 ∈ Locally 𝐴 ∧ 𝑣 ∈ 𝑆 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑣 ) → ∃ 𝑠 ∈ 𝑆 ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) )
19	14 15 17 18	syl3anc	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ∃ 𝑠 ∈ 𝑆 ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) )
20		reeanv	⊢ ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ↔ ( ∃ 𝑟 ∈ 𝑅 ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) )
21	2	ad3antrrr	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑅 ∈ Top )
22	3	ad3antlr	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑆 ∈ Top )
23		simprll	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑟 ∈ 𝑅 )
24		simprlr	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑠 ∈ 𝑆 )
25		txopn	⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝑟 × 𝑠 ) ∈ ( 𝑅 ×_t 𝑆 ) )
26	21 22 23 24 25	syl22anc	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( 𝑟 × 𝑠 ) ∈ ( 𝑅 ×_t 𝑆 ) )
27		simprl1	⊢ ( ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑟 ⊆ 𝑢 )
28		simprr1	⊢ ( ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠 ⊆ 𝑣 )
29		xpss12	⊢ ( ( 𝑟 ⊆ 𝑢 ∧ 𝑠 ⊆ 𝑣 ) → ( 𝑟 × 𝑠 ) ⊆ ( 𝑢 × 𝑣 ) )
30	27 28 29	syl2anc	⊢ ( ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑟 × 𝑠 ) ⊆ ( 𝑢 × 𝑣 ) )
31		simprrr	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( 𝑢 × 𝑣 ) ⊆ 𝑥 )
32	30 31	sylan9ssr	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( 𝑟 × 𝑠 ) ⊆ 𝑥 )
33		vex	⊢ 𝑥 ∈ V
34	33	elpw2	⊢ ( ( 𝑟 × 𝑠 ) ∈ 𝒫 𝑥 ↔ ( 𝑟 × 𝑠 ) ⊆ 𝑥 )
35	32 34	sylibr	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( 𝑟 × 𝑠 ) ∈ 𝒫 𝑥 )
36	26 35	elind	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( 𝑟 × 𝑠 ) ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) )
37		1st2nd2	⊢ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
38	9 37	syl	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
39	38	adantr	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑦 = ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ )
40		simprl2	⊢ ( ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) → ( 1^st ‘ 𝑦 ) ∈ 𝑟 )
41		simprr2	⊢ ( ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) → ( 2^nd ‘ 𝑦 ) ∈ 𝑠 )
42	40 41	opelxpd	⊢ ( ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) → ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∈ ( 𝑟 × 𝑠 ) )
43	42	adantl	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → ⟨ ( 1^st ‘ 𝑦 ) , ( 2^nd ‘ 𝑦 ) ⟩ ∈ ( 𝑟 × 𝑠 ) )
44	39 43	eqeltrd	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑦 ∈ ( 𝑟 × 𝑠 ) )
45		txrest	⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( 𝑅 ×_t 𝑆 ) ↾_t ( 𝑟 × 𝑠 ) ) = ( ( 𝑅 ↾_t 𝑟 ) ×_t ( 𝑆 ↾_t 𝑠 ) ) )
46	21 22 23 24 45	syl22anc	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( ( 𝑅 ×_t 𝑆 ) ↾_t ( 𝑟 × 𝑠 ) ) = ( ( 𝑅 ↾_t 𝑟 ) ×_t ( 𝑆 ↾_t 𝑠 ) ) )
47		simprl3	⊢ ( ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 )
48		simprr3	⊢ ( ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 )
49	1	caovcl	⊢ ( ( ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) → ( ( 𝑅 ↾_t 𝑟 ) ×_t ( 𝑆 ↾_t 𝑠 ) ) ∈ 𝐴 )
50	47 48 49	syl2anc	⊢ ( ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) → ( ( 𝑅 ↾_t 𝑟 ) ×_t ( 𝑆 ↾_t 𝑠 ) ) ∈ 𝐴 )
51	50	adantl	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( ( 𝑅 ↾_t 𝑟 ) ×_t ( 𝑆 ↾_t 𝑠 ) ) ∈ 𝐴 )
52	46 51	eqeltrd	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( ( 𝑅 ×_t 𝑆 ) ↾_t ( 𝑟 × 𝑠 ) ) ∈ 𝐴 )
53		eleq2	⊢ ( 𝑧 = ( 𝑟 × 𝑠 ) → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ ( 𝑟 × 𝑠 ) ) )
54		oveq2	⊢ ( 𝑧 = ( 𝑟 × 𝑠 ) → ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) = ( ( 𝑅 ×_t 𝑆 ) ↾_t ( 𝑟 × 𝑠 ) ) )
55	54	eleq1d	⊢ ( 𝑧 = ( 𝑟 × 𝑠 ) → ( ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ↔ ( ( 𝑅 ×_t 𝑆 ) ↾_t ( 𝑟 × 𝑠 ) ) ∈ 𝐴 ) )
56	53 55	anbi12d	⊢ ( 𝑧 = ( 𝑟 × 𝑠 ) → ( ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) ↔ ( 𝑦 ∈ ( 𝑟 × 𝑠 ) ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t ( 𝑟 × 𝑠 ) ) ∈ 𝐴 ) ) )
57	56	rspcev	⊢ ( ( ( 𝑟 × 𝑠 ) ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ∧ ( 𝑦 ∈ ( 𝑟 × 𝑠 ) ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t ( 𝑟 × 𝑠 ) ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) )
58	36 44 52 57	syl12anc	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ∧ ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) ) ) → ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) )
59	58	expr	⊢ ( ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) ) )
60	59	rexlimdvva	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 ( ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) ) )
61	20 60	biimtrrid	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( ( ∃ 𝑟 ∈ 𝑅 ( 𝑟 ⊆ 𝑢 ∧ ( 1^st ‘ 𝑦 ) ∈ 𝑟 ∧ ( 𝑅 ↾_t 𝑟 ) ∈ 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑆 ( 𝑠 ⊆ 𝑣 ∧ ( 2^nd ‘ 𝑦 ) ∈ 𝑠 ∧ ( 𝑆 ↾_t 𝑠 ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) ) )
62	13 19 61	mp2and	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) )
63	62	expr	⊢ ( ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) ∧ ( 𝑢 ∈ 𝑅 ∧ 𝑣 ∈ 𝑆 ) ) → ( ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) → ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) ) )
64	63	rexlimdvva	⊢ ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) → ( ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) → ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) ) )
65	64	ralimdv	⊢ ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) → ( ∀ 𝑦 ∈ 𝑥 ∃ 𝑢 ∈ 𝑅 ∃ 𝑣 ∈ 𝑆 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) ) )
66	6 65	sylbid	⊢ ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) → ( 𝑥 ∈ ( 𝑅 ×_t 𝑆 ) → ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) ) )
67	66	ralrimiv	⊢ ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) → ∀ 𝑥 ∈ ( 𝑅 ×_t 𝑆 ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) )
68		islly	⊢ ( ( 𝑅 ×_t 𝑆 ) ∈ Locally 𝐴 ↔ ( ( 𝑅 ×_t 𝑆 ) ∈ Top ∧ ∀ 𝑥 ∈ ( 𝑅 ×_t 𝑆 ) ∀ 𝑦 ∈ 𝑥 ∃ 𝑧 ∈ ( ( 𝑅 ×_t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦 ∈ 𝑧 ∧ ( ( 𝑅 ×_t 𝑆 ) ↾_t 𝑧 ) ∈ 𝐴 ) ) )
69	5 67 68	sylanbrc	⊢ ( ( 𝑅 ∈ Locally 𝐴 ∧ 𝑆 ∈ Locally 𝐴 ) → ( 𝑅 ×_t 𝑆 ) ∈ Locally 𝐴 )

Metamath Proof Explorer

Theorem txlly

Proof