Step | Hyp | Ref
| Expression |
1 | | xmetxp.p |
. . 3
⊢ 𝑃 = (𝑢 ∈ (𝑋 × 𝑌), 𝑣 ∈ (𝑋 × 𝑌) ↦ sup({((1st ‘𝑢)𝑀(1st ‘𝑣)), ((2nd ‘𝑢)𝑁(2nd ‘𝑣))}, ℝ*, <
)) |
2 | | xmetxp.1 |
. . 3
⊢ (𝜑 → 𝑀 ∈ (∞Met‘𝑋)) |
3 | | xmetxp.2 |
. . 3
⊢ (𝜑 → 𝑁 ∈ (∞Met‘𝑌)) |
4 | | xmettx.j |
. . 3
⊢ 𝐽 = (MetOpen‘𝑀) |
5 | | xmettx.k |
. . 3
⊢ 𝐾 = (MetOpen‘𝑁) |
6 | | xmettx.l |
. . 3
⊢ 𝐿 = (MetOpen‘𝑃) |
7 | 1, 2, 3, 4, 5, 6 | xmettxlem 12951 |
. 2
⊢ (𝜑 → 𝐿 ⊆ (𝐽 ×t 𝐾)) |
8 | | eqid 2157 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) = (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) |
9 | 8 | elrnmpog 5934 |
. . . . . . . . . . 11
⊢ (𝑤 ∈ V → (𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ↔ ∃𝑟 ∈ 𝐽 ∃𝑠 ∈ 𝐾 𝑤 = (𝑟 × 𝑠))) |
10 | 9 | elv 2716 |
. . . . . . . . . 10
⊢ (𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ↔ ∃𝑟 ∈ 𝐽 ∃𝑠 ∈ 𝐾 𝑤 = (𝑟 × 𝑠)) |
11 | 10 | biimpi 119 |
. . . . . . . . 9
⊢ (𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) → ∃𝑟 ∈ 𝐽 ∃𝑠 ∈ 𝐾 𝑤 = (𝑟 × 𝑠)) |
12 | 11 | adantl 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) → ∃𝑟 ∈ 𝐽 ∃𝑠 ∈ 𝐾 𝑤 = (𝑟 × 𝑠)) |
13 | | xpeq1 4601 |
. . . . . . . . . 10
⊢ (𝑟 = 𝑥 → (𝑟 × 𝑠) = (𝑥 × 𝑠)) |
14 | 13 | eqeq2d 2169 |
. . . . . . . . 9
⊢ (𝑟 = 𝑥 → (𝑤 = (𝑟 × 𝑠) ↔ 𝑤 = (𝑥 × 𝑠))) |
15 | | xpeq2 4602 |
. . . . . . . . . 10
⊢ (𝑠 = 𝑦 → (𝑥 × 𝑠) = (𝑥 × 𝑦)) |
16 | 15 | eqeq2d 2169 |
. . . . . . . . 9
⊢ (𝑠 = 𝑦 → (𝑤 = (𝑥 × 𝑠) ↔ 𝑤 = (𝑥 × 𝑦))) |
17 | 14, 16 | cbvrex2v 2692 |
. . . . . . . 8
⊢
(∃𝑟 ∈
𝐽 ∃𝑠 ∈ 𝐾 𝑤 = (𝑟 × 𝑠) ↔ ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐾 𝑤 = (𝑥 × 𝑦)) |
18 | 12, 17 | sylib 121 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) → ∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐾 𝑤 = (𝑥 × 𝑦)) |
19 | | simpr 109 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → 𝑤 = (𝑥 × 𝑦)) |
20 | | simplll 523 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → 𝜑) |
21 | | simplrl 525 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → 𝑥 ∈ 𝐽) |
22 | | simplrr 526 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → 𝑦 ∈ 𝐾) |
23 | 4 | mopntopon 12885 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑀 ∈ (∞Met‘𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
24 | 2, 23 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
25 | 24 | adantr 274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝐽 ∈ (TopOn‘𝑋)) |
26 | | simprl 521 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑥 ∈ 𝐽) |
27 | | toponss 12466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝑥 ∈ 𝐽) → 𝑥 ⊆ 𝑋) |
28 | 25, 26, 27 | syl2anc 409 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑥 ⊆ 𝑋) |
29 | 5 | mopntopon 12885 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝐾 ∈ (TopOn‘𝑌)) |
30 | 3, 29 | syl 14 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
31 | 30 | adantr 274 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝐾 ∈ (TopOn‘𝑌)) |
32 | | simprr 522 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑦 ∈ 𝐾) |
33 | | toponss 12466 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐾 ∈ (TopOn‘𝑌) ∧ 𝑦 ∈ 𝐾) → 𝑦 ⊆ 𝑌) |
34 | 31, 32, 33 | syl2anc 409 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → 𝑦 ⊆ 𝑌) |
35 | | xpss12 4694 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ⊆ 𝑋 ∧ 𝑦 ⊆ 𝑌) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌)) |
36 | 28, 34, 35 | syl2anc 409 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝑥 × 𝑦) ⊆ (𝑋 × 𝑌)) |
37 | 1, 2, 3 | xmetxp 12949 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌))) |
38 | | unirnbl 12865 |
. . . . . . . . . . . . . . . 16
⊢ (𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) → ∪ ran
(ball‘𝑃) = (𝑋 × 𝑌)) |
39 | 37, 38 | syl 14 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∪ ran (ball‘𝑃) = (𝑋 × 𝑌)) |
40 | 39 | adantr 274 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ∪ ran
(ball‘𝑃) = (𝑋 × 𝑌)) |
41 | 36, 40 | sseqtrrd 3167 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝑥 × 𝑦) ⊆ ∪ ran
(ball‘𝑃)) |
42 | 2 | ad2antrr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑀 ∈ (∞Met‘𝑋)) |
43 | | simplrl 525 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑥 ∈ 𝐽) |
44 | | xp1st 6114 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑗 ∈ (𝑥 × 𝑦) → (1st ‘𝑗) ∈ 𝑥) |
45 | 44 | adantl 275 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → (1st ‘𝑗) ∈ 𝑥) |
46 | 4 | mopni2 12925 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑀 ∈ (∞Met‘𝑋) ∧ 𝑥 ∈ 𝐽 ∧ (1st ‘𝑗) ∈ 𝑥) → ∃𝑚 ∈ ℝ+ ((1st
‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥) |
47 | 42, 43, 45, 46 | syl3anc 1220 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → ∃𝑚 ∈ ℝ+ ((1st
‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥) |
48 | 3 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑁 ∈ (∞Met‘𝑌)) |
49 | | simplrr 526 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑦 ∈ 𝐾) |
50 | | xp2nd 6115 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑗 ∈ (𝑥 × 𝑦) → (2nd ‘𝑗) ∈ 𝑦) |
51 | 50 | adantl 275 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → (2nd ‘𝑗) ∈ 𝑦) |
52 | 5 | mopni2 12925 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈ (∞Met‘𝑌) ∧ 𝑦 ∈ 𝐾 ∧ (2nd ‘𝑗) ∈ 𝑦) → ∃𝑛 ∈ ℝ+ ((2nd
‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦) |
53 | 48, 49, 51, 52 | syl3anc 1220 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → ∃𝑛 ∈ ℝ+ ((2nd
‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦) |
54 | 53 | adantr 274 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) → ∃𝑛 ∈ ℝ+ ((2nd
‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦) |
55 | | blf 12852 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) → (ball‘𝑃):((𝑋 × 𝑌) ×
ℝ*)⟶𝒫 (𝑋 × 𝑌)) |
56 | 37, 55 | syl 14 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (ball‘𝑃):((𝑋 × 𝑌) ×
ℝ*)⟶𝒫 (𝑋 × 𝑌)) |
57 | 56 | ffnd 5321 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (ball‘𝑃) Fn ((𝑋 × 𝑌) ×
ℝ*)) |
58 | 57 | ad4antr 486 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (ball‘𝑃) Fn ((𝑋 × 𝑌) ×
ℝ*)) |
59 | 36 | sselda 3128 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑗 ∈ (𝑋 × 𝑌)) |
60 | 59 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑗 ∈ (𝑋 × 𝑌)) |
61 | | rpxr 9569 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑚 ∈ ℝ+
→ 𝑚 ∈
ℝ*) |
62 | 61 | ad2antrl 482 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) → 𝑚 ∈ ℝ*) |
63 | 62 | adantr 274 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑚 ∈ ℝ*) |
64 | | rpxr 9569 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 ∈ ℝ+
→ 𝑛 ∈
ℝ*) |
65 | 64 | ad2antrl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑛 ∈ ℝ*) |
66 | | xrmincl 11167 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑚 ∈ ℝ*
∧ 𝑛 ∈
ℝ*) → inf({𝑚, 𝑛}, ℝ*, < ) ∈
ℝ*) |
67 | 63, 65, 66 | syl2anc 409 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → inf({𝑚, 𝑛}, ℝ*, < ) ∈
ℝ*) |
68 | | fnovrn 5969 |
. . . . . . . . . . . . . . . . . 18
⊢
(((ball‘𝑃) Fn
((𝑋 × 𝑌) × ℝ*)
∧ 𝑗 ∈ (𝑋 × 𝑌) ∧ inf({𝑚, 𝑛}, ℝ*, < ) ∈
ℝ*) → (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) ∈ ran
(ball‘𝑃)) |
69 | 58, 60, 67, 68 | syl3anc 1220 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) ∈ ran
(ball‘𝑃)) |
70 | | eleq2 2221 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) → (𝑗 ∈ 𝑘 ↔ 𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, <
)))) |
71 | | sseq1 3151 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) → (𝑘 ⊆ (𝑥 × 𝑦) ↔ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) ⊆
(𝑥 × 𝑦))) |
72 | 70, 71 | anbi12d 465 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) →
((𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦)) ↔ (𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) ∧ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) ⊆
(𝑥 × 𝑦)))) |
73 | 72 | adantl 275 |
. . . . . . . . . . . . . . . . 17
⊢
((((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) ∧ 𝑘 = (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < ))) →
((𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦)) ↔ (𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) ∧ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) ⊆
(𝑥 × 𝑦)))) |
74 | 37 | ad4antr 486 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑃 ∈ (∞Met‘(𝑋 × 𝑌))) |
75 | | simplrl 525 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑚 ∈ ℝ+) |
76 | | simprl 521 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑛 ∈ ℝ+) |
77 | | xrminrpcl 11175 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑚 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → inf({𝑚, 𝑛}, ℝ*, < ) ∈
ℝ+) |
78 | 75, 76, 77 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → inf({𝑚, 𝑛}, ℝ*, < ) ∈
ℝ+) |
79 | | blcntr 12858 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) ∧ 𝑗 ∈ (𝑋 × 𝑌) ∧ inf({𝑚, 𝑛}, ℝ*, < ) ∈
ℝ+) → 𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, <
))) |
80 | 74, 60, 78, 79 | syl3anc 1220 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, <
))) |
81 | 42 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑀 ∈ (∞Met‘𝑋)) |
82 | 48 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → 𝑁 ∈ (∞Met‘𝑌)) |
83 | 1, 81, 82, 67, 60 | xmetxpbl 12950 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) =
(((1st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ*, < )) ×
((2nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ*, <
)))) |
84 | 28 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑥 ⊆ 𝑋) |
85 | 84, 45 | sseldd 3129 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → (1st ‘𝑗) ∈ 𝑋) |
86 | 85 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (1st ‘𝑗) ∈ 𝑋) |
87 | | xrmin1inf 11168 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 ∈ ℝ*
∧ 𝑛 ∈
ℝ*) → inf({𝑚, 𝑛}, ℝ*, < ) ≤ 𝑚) |
88 | 63, 65, 87 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → inf({𝑚, 𝑛}, ℝ*, < ) ≤ 𝑚) |
89 | | ssbl 12868 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑀 ∈ (∞Met‘𝑋) ∧ (1st
‘𝑗) ∈ 𝑋) ∧ (inf({𝑚, 𝑛}, ℝ*, < ) ∈
ℝ* ∧ 𝑚
∈ ℝ*) ∧ inf({𝑚, 𝑛}, ℝ*, < ) ≤ 𝑚) → ((1st
‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ*, < )) ⊆
((1st ‘𝑗)(ball‘𝑀)𝑚)) |
90 | 81, 86, 67, 63, 88, 89 | syl221anc 1231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((1st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ*, < )) ⊆
((1st ‘𝑗)(ball‘𝑀)𝑚)) |
91 | | simplrr 526 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥) |
92 | 90, 91 | sstrd 3138 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((1st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ*, < )) ⊆ 𝑥) |
93 | 34 | adantr 274 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → 𝑦 ⊆ 𝑌) |
94 | 93, 51 | sseldd 3129 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → (2nd ‘𝑗) ∈ 𝑌) |
95 | 94 | ad2antrr 480 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (2nd ‘𝑗) ∈ 𝑌) |
96 | | xrmin2inf 11169 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑚 ∈ ℝ*
∧ 𝑛 ∈
ℝ*) → inf({𝑚, 𝑛}, ℝ*, < ) ≤ 𝑛) |
97 | 63, 65, 96 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → inf({𝑚, 𝑛}, ℝ*, < ) ≤ 𝑛) |
98 | | ssbl 12868 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑁 ∈ (∞Met‘𝑌) ∧ (2nd
‘𝑗) ∈ 𝑌) ∧ (inf({𝑚, 𝑛}, ℝ*, < ) ∈
ℝ* ∧ 𝑛
∈ ℝ*) ∧ inf({𝑚, 𝑛}, ℝ*, < ) ≤ 𝑛) → ((2nd
‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ*, < )) ⊆
((2nd ‘𝑗)(ball‘𝑁)𝑛)) |
99 | 82, 95, 67, 65, 97, 98 | syl221anc 1231 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((2nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ*, < )) ⊆
((2nd ‘𝑗)(ball‘𝑁)𝑛)) |
100 | | simprr 522 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦) |
101 | 99, 100 | sstrd 3138 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ((2nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ*, < )) ⊆ 𝑦) |
102 | | xpss12 4694 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((1st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ*, < )) ⊆ 𝑥 ∧ ((2nd
‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ*, < )) ⊆ 𝑦) → (((1st
‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ*, < )) ×
((2nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ*, < ))) ⊆
(𝑥 × 𝑦)) |
103 | 92, 101, 102 | syl2anc 409 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (((1st ‘𝑗)(ball‘𝑀)inf({𝑚, 𝑛}, ℝ*, < )) ×
((2nd ‘𝑗)(ball‘𝑁)inf({𝑚, 𝑛}, ℝ*, < ))) ⊆
(𝑥 × 𝑦)) |
104 | 83, 103 | eqsstrd 3164 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) ⊆
(𝑥 × 𝑦)) |
105 | 80, 104 | jca 304 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → (𝑗 ∈ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) ∧ (𝑗(ball‘𝑃)inf({𝑚, 𝑛}, ℝ*, < )) ⊆
(𝑥 × 𝑦))) |
106 | 69, 73, 105 | rspcedvd 2822 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) ∧ (𝑛 ∈ ℝ+ ∧
((2nd ‘𝑗)(ball‘𝑁)𝑛) ⊆ 𝑦)) → ∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦))) |
107 | 54, 106 | rexlimddv 2579 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) ∧ (𝑚 ∈ ℝ+ ∧
((1st ‘𝑗)(ball‘𝑀)𝑚) ⊆ 𝑥)) → ∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦))) |
108 | 47, 107 | rexlimddv 2579 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑗 ∈ (𝑥 × 𝑦)) → ∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦))) |
109 | 108 | ralrimiva 2530 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ∀𝑗 ∈ (𝑥 × 𝑦)∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦))) |
110 | 41, 109 | jca 304 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ((𝑥 × 𝑦) ⊆ ∪ ran
(ball‘𝑃) ∧
∀𝑗 ∈ (𝑥 × 𝑦)∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦)))) |
111 | | blex 12829 |
. . . . . . . . . . . . . . 15
⊢ (𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) → (ball‘𝑃) ∈ V) |
112 | 37, 111 | syl 14 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (ball‘𝑃) ∈ V) |
113 | 112 | adantr 274 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (ball‘𝑃) ∈ V) |
114 | | rnexg 4852 |
. . . . . . . . . . . . 13
⊢
((ball‘𝑃)
∈ V → ran (ball‘𝑃) ∈ V) |
115 | | eltg2 12495 |
. . . . . . . . . . . . 13
⊢ (ran
(ball‘𝑃) ∈ V
→ ((𝑥 × 𝑦) ∈ (topGen‘ran
(ball‘𝑃)) ↔
((𝑥 × 𝑦) ⊆ ∪ ran (ball‘𝑃) ∧ ∀𝑗 ∈ (𝑥 × 𝑦)∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦))))) |
116 | 113, 114,
115 | 3syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → ((𝑥 × 𝑦) ∈ (topGen‘ran (ball‘𝑃)) ↔ ((𝑥 × 𝑦) ⊆ ∪ ran
(ball‘𝑃) ∧
∀𝑗 ∈ (𝑥 × 𝑦)∃𝑘 ∈ ran (ball‘𝑃)(𝑗 ∈ 𝑘 ∧ 𝑘 ⊆ (𝑥 × 𝑦))))) |
117 | 110, 116 | mpbird 166 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝑥 × 𝑦) ∈ (topGen‘ran (ball‘𝑃))) |
118 | 20, 21, 22, 117 | syl12anc 1218 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → (𝑥 × 𝑦) ∈ (topGen‘ran (ball‘𝑃))) |
119 | 19, 118 | eqeltrd 2234 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) ∧ 𝑤 = (𝑥 × 𝑦)) → 𝑤 ∈ (topGen‘ran (ball‘𝑃))) |
120 | 119 | ex 114 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ∧ (𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝐾)) → (𝑤 = (𝑥 × 𝑦) → 𝑤 ∈ (topGen‘ran (ball‘𝑃)))) |
121 | 120 | rexlimdvva 2582 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) → (∃𝑥 ∈ 𝐽 ∃𝑦 ∈ 𝐾 𝑤 = (𝑥 × 𝑦) → 𝑤 ∈ (topGen‘ran (ball‘𝑃)))) |
122 | 18, 121 | mpd 13 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) → 𝑤 ∈ (topGen‘ran (ball‘𝑃))) |
123 | 122 | ex 114 |
. . . . 5
⊢ (𝜑 → (𝑤 ∈ ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) → 𝑤 ∈ (topGen‘ran (ball‘𝑃)))) |
124 | 123 | ssrdv 3134 |
. . . 4
⊢ (𝜑 → ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ⊆ (topGen‘ran
(ball‘𝑃))) |
125 | 4 | mopntop 12886 |
. . . . . . . 8
⊢ (𝑀 ∈ (∞Met‘𝑋) → 𝐽 ∈ Top) |
126 | 2, 125 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝐽 ∈ Top) |
127 | 5 | mopntop 12886 |
. . . . . . . 8
⊢ (𝑁 ∈ (∞Met‘𝑌) → 𝐾 ∈ Top) |
128 | 3, 127 | syl 14 |
. . . . . . 7
⊢ (𝜑 → 𝐾 ∈ Top) |
129 | | mpoexga 6161 |
. . . . . . 7
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V) |
130 | 126, 128,
129 | syl2anc 409 |
. . . . . 6
⊢ (𝜑 → (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V) |
131 | | rnexg 4852 |
. . . . . 6
⊢ ((𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V → ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V) |
132 | 130, 131 | syl 14 |
. . . . 5
⊢ (𝜑 → ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V) |
133 | 37, 111, 114 | 3syl 17 |
. . . . 5
⊢ (𝜑 → ran (ball‘𝑃) ∈ V) |
134 | | tgss3 12520 |
. . . . 5
⊢ ((ran
(𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ∈ V ∧ ran (ball‘𝑃) ∈ V) →
((topGen‘ran (𝑟
∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ⊆ (topGen‘ran
(ball‘𝑃)) ↔ ran
(𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ⊆ (topGen‘ran
(ball‘𝑃)))) |
135 | 132, 133,
134 | syl2anc 409 |
. . . 4
⊢ (𝜑 → ((topGen‘ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ⊆ (topGen‘ran
(ball‘𝑃)) ↔ ran
(𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) ⊆ (topGen‘ran
(ball‘𝑃)))) |
136 | 124, 135 | mpbird 166 |
. . 3
⊢ (𝜑 → (topGen‘ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠))) ⊆ (topGen‘ran
(ball‘𝑃))) |
137 | | eqid 2157 |
. . . . 5
⊢ ran
(𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) = ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)) |
138 | 137 | txval 12697 |
. . . 4
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ×t 𝐾) = (topGen‘ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)))) |
139 | 126, 128,
138 | syl2anc 409 |
. . 3
⊢ (𝜑 → (𝐽 ×t 𝐾) = (topGen‘ran (𝑟 ∈ 𝐽, 𝑠 ∈ 𝐾 ↦ (𝑟 × 𝑠)))) |
140 | 6 | mopnval 12884 |
. . . 4
⊢ (𝑃 ∈ (∞Met‘(𝑋 × 𝑌)) → 𝐿 = (topGen‘ran (ball‘𝑃))) |
141 | 37, 140 | syl 14 |
. . 3
⊢ (𝜑 → 𝐿 = (topGen‘ran (ball‘𝑃))) |
142 | 136, 139,
141 | 3sstr4d 3173 |
. 2
⊢ (𝜑 → (𝐽 ×t 𝐾) ⊆ 𝐿) |
143 | 7, 142 | eqssd 3145 |
1
⊢ (𝜑 → 𝐿 = (𝐽 ×t 𝐾)) |