Metamath Proof Explorer


Theorem 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 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) → ( 1st𝑦 ) ∈ 𝑢 )
11 9 10 syl ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( 1st𝑦 ) ∈ 𝑢 )
12 llyi ( ( 𝑅 ∈ Locally 𝐴𝑢𝑅 ∧ ( 1st𝑦 ) ∈ 𝑢 ) → ∃ 𝑟𝑅 ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) )
13 7 8 11 12 syl3anc ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ∃ 𝑟𝑅 ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) )
14 simplr ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑆 ∈ Locally 𝐴 )
15 simprlr ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑣𝑆 )
16 xp2nd ( 𝑦 ∈ ( 𝑢 × 𝑣 ) → ( 2nd𝑦 ) ∈ 𝑣 )
17 9 16 syl ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( 2nd𝑦 ) ∈ 𝑣 )
18 llyi ( ( 𝑆 ∈ Locally 𝐴𝑣𝑆 ∧ ( 2nd𝑦 ) ∈ 𝑣 ) → ∃ 𝑠𝑆 ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) )
19 14 15 17 18 syl3anc ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ∃ 𝑠𝑆 ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) )
20 reeanv ( ∃ 𝑟𝑅𝑠𝑆 ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ↔ ( ∃ 𝑟𝑅 ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ∃ 𝑠𝑆 ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) )
21 2 ad3antrrr ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑅 ∈ Top )
22 3 ad3antlr ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑆 ∈ Top )
23 simprll ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑟𝑅 )
24 simprlr ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑠𝑆 )
25 txopn ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑟𝑅𝑠𝑆 ) ) → ( 𝑟 × 𝑠 ) ∈ ( 𝑅 ×t 𝑆 ) )
26 21 22 23 24 25 syl22anc ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( 𝑟 × 𝑠 ) ∈ ( 𝑅 ×t 𝑆 ) )
27 simprl1 ( ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑟𝑢 )
28 simprr1 ( ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) → 𝑠𝑣 )
29 xpss12 ( ( 𝑟𝑢𝑠𝑣 ) → ( 𝑟 × 𝑠 ) ⊆ ( 𝑢 × 𝑣 ) )
30 27 28 29 syl2anc ( ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑟 × 𝑠 ) ⊆ ( 𝑢 × 𝑣 ) )
31 simprrr ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( 𝑢 × 𝑣 ) ⊆ 𝑥 )
32 30 31 sylan9ssr ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( 𝑟 × 𝑠 ) ⊆ 𝑥 )
33 vex 𝑥 ∈ V
34 33 elpw2 ( ( 𝑟 × 𝑠 ) ∈ 𝒫 𝑥 ↔ ( 𝑟 × 𝑠 ) ⊆ 𝑥 )
35 32 34 sylibr ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( 𝑟 × 𝑠 ) ∈ 𝒫 𝑥 )
36 26 35 elind ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( 𝑟 × 𝑠 ) ∈ ( ( 𝑅 ×t 𝑆 ) ∩ 𝒫 𝑥 ) )
37 1st2nd2 ( 𝑦 ∈ ( 𝑢 × 𝑣 ) → 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
38 9 37 syl ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
39 38 adantr ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑦 = ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ )
40 simprl2 ( ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) → ( 1st𝑦 ) ∈ 𝑟 )
41 simprr2 ( ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) → ( 2nd𝑦 ) ∈ 𝑠 )
42 40 41 opelxpd ( ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) → ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ ∈ ( 𝑟 × 𝑠 ) )
43 42 adantl ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → ⟨ ( 1st𝑦 ) , ( 2nd𝑦 ) ⟩ ∈ ( 𝑟 × 𝑠 ) )
44 39 43 eqeltrd ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → 𝑦 ∈ ( 𝑟 × 𝑠 ) )
45 txrest ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) ∧ ( 𝑟𝑅𝑠𝑆 ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑟 × 𝑠 ) ) = ( ( 𝑅t 𝑟 ) ×t ( 𝑆t 𝑠 ) ) )
46 21 22 23 24 45 syl22anc ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝑟 × 𝑠 ) ) = ( ( 𝑅t 𝑟 ) ×t ( 𝑆t 𝑠 ) ) )
47 simprl3 ( ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑅t 𝑟 ) ∈ 𝐴 )
48 simprr3 ( ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) → ( 𝑆t 𝑠 ) ∈ 𝐴 )
49 1 caovcl ( ( ( 𝑅t 𝑟 ) ∈ 𝐴 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) → ( ( 𝑅t 𝑟 ) ×t ( 𝑆t 𝑠 ) ) ∈ 𝐴 )
50 47 48 49 syl2anc ( ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) → ( ( 𝑅t 𝑟 ) ×t ( 𝑆t 𝑠 ) ) ∈ 𝐴 )
51 50 adantl ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → ( ( 𝑅t 𝑟 ) ×t ( 𝑆t 𝑠 ) ) ∈ 𝐴 )
52 46 51 eqeltrd ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆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 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( ( 𝑟𝑅𝑠𝑆 ) ∧ ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) ) ) → ∃ 𝑧 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦𝑧 ∧ ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) )
59 58 expr ( ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) ∧ ( 𝑟𝑅𝑠𝑆 ) ) → ( ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦𝑧 ∧ ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) ) )
60 59 rexlimdvva ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( ∃ 𝑟𝑅𝑠𝑆 ( ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆t 𝑠 ) ∈ 𝐴 ) ) → ∃ 𝑧 ∈ ( ( 𝑅 ×t 𝑆 ) ∩ 𝒫 𝑥 ) ( 𝑦𝑧 ∧ ( ( 𝑅 ×t 𝑆 ) ↾t 𝑧 ) ∈ 𝐴 ) ) )
61 20 60 syl5bir ( ( ( 𝑅 ∈ Locally 𝐴𝑆 ∈ Locally 𝐴 ) ∧ ( ( 𝑢𝑅𝑣𝑆 ) ∧ ( 𝑦 ∈ ( 𝑢 × 𝑣 ) ∧ ( 𝑢 × 𝑣 ) ⊆ 𝑥 ) ) ) → ( ( ∃ 𝑟𝑅 ( 𝑟𝑢 ∧ ( 1st𝑦 ) ∈ 𝑟 ∧ ( 𝑅t 𝑟 ) ∈ 𝐴 ) ∧ ∃ 𝑠𝑆 ( 𝑠𝑣 ∧ ( 2nd𝑦 ) ∈ 𝑠 ∧ ( 𝑆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 𝐴 )