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 𝐴 ) |