Step | Hyp | Ref
| Expression |
1 | | ptrecube.r |
. . . 4
⊢ 𝑅 =
(∏t‘((1...𝑁) × {(topGen‘ran
(,))})) |
2 | | fzfi 13432 |
. . . . 5
⊢
(1...𝑁) ∈
Fin |
3 | | retop 23515 |
. . . . . 6
⊢
(topGen‘ran (,)) ∈ Top |
4 | | fnconstg 6567 |
. . . . . 6
⊢
((topGen‘ran (,)) ∈ Top → ((1...𝑁) × {(topGen‘ran (,))}) Fn
(1...𝑁)) |
5 | 3, 4 | ax-mp 5 |
. . . . 5
⊢
((1...𝑁) ×
{(topGen‘ran (,))}) Fn (1...𝑁) |
6 | | eqid 2738 |
. . . . . 6
⊢ {𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))} = {𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))} |
7 | 6 | ptval 22322 |
. . . . 5
⊢
(((1...𝑁) ∈ Fin
∧ ((1...𝑁) ×
{(topGen‘ran (,))}) Fn (1...𝑁)) →
(∏t‘((1...𝑁) × {(topGen‘ran (,))})) =
(topGen‘{𝑥 ∣
∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))})) |
8 | 2, 5, 7 | mp2an 692 |
. . . 4
⊢
(∏t‘((1...𝑁) × {(topGen‘ran (,))})) =
(topGen‘{𝑥 ∣
∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))}) |
9 | 1, 8 | eqtri 2761 |
. . 3
⊢ 𝑅 = (topGen‘{𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))}) |
10 | 9 | eleq2i 2824 |
. 2
⊢ (𝑆 ∈ 𝑅 ↔ 𝑆 ∈ (topGen‘{𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))})) |
11 | | tg2 21717 |
. . 3
⊢ ((𝑆 ∈ (topGen‘{𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))}) ∧ 𝑃 ∈ 𝑆) → ∃𝑧 ∈ {𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))} (𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆)) |
12 | 6 | elpt 22324 |
. . . . 5
⊢ (𝑧 ∈ {𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))} ↔ ∃𝑔((𝑔 Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑧 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑧)(𝑔‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑧 = X𝑛 ∈
(1...𝑁)(𝑔‘𝑛))) |
13 | | fvex 6688 |
. . . . . . . . . . . . . . 15
⊢
(topGen‘ran (,)) ∈ V |
14 | 13 | fvconst2 6977 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) =
(topGen‘ran (,))) |
15 | 14 | eleq2d 2818 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑁) → ((𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ↔
(𝑔‘𝑛) ∈ (topGen‘ran
(,)))) |
16 | 15 | ralbiia 3079 |
. . . . . . . . . . . 12
⊢
(∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ↔
∀𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∈ (topGen‘ran
(,))) |
17 | | elixp2 8512 |
. . . . . . . . . . . . . 14
⊢ (𝑃 ∈ X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ↔ (𝑃 ∈ V ∧ 𝑃 Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(𝑃‘𝑛) ∈ (𝑔‘𝑛))) |
18 | 17 | simp3bi 1148 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∈ X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) → ∀𝑛 ∈ (1...𝑁)(𝑃‘𝑛) ∈ (𝑔‘𝑛)) |
19 | | r19.26 3084 |
. . . . . . . . . . . . . 14
⊢
(∀𝑛 ∈
(1...𝑁)((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) ↔ (∀𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧
∀𝑛 ∈ (1...𝑁)(𝑃‘𝑛) ∈ (𝑔‘𝑛))) |
20 | | uniretop 23516 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℝ =
∪ (topGen‘ran (,)) |
21 | 20 | eltopss 21659 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((topGen‘ran (,)) ∈ Top ∧ (𝑔‘𝑛) ∈ (topGen‘ran (,))) →
(𝑔‘𝑛) ⊆ ℝ) |
22 | 3, 21 | mpan 690 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔‘𝑛) ∈ (topGen‘ran (,)) → (𝑔‘𝑛) ⊆ ℝ) |
23 | 22 | sselda 3878 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → (𝑃‘𝑛) ∈ ℝ) |
24 | | ptrecube.d |
. . . . . . . . . . . . . . . . . . . 20
⊢ 𝐷 = ((abs ∘ − )
↾ (ℝ × ℝ)) |
25 | 24 | rexmet 23544 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝐷 ∈
(∞Met‘ℝ) |
26 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) |
27 | 24, 26 | tgioo 23549 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(topGen‘ran (,)) = (MetOpen‘𝐷) |
28 | 27 | mopni2 23247 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈
(∞Met‘ℝ) ∧ (𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑦 ∈ ℝ+ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛)) |
29 | 25, 28 | mp3an1 1449 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑦 ∈ ℝ+ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛)) |
30 | | r19.42v 3254 |
. . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦 ∈
ℝ+ ((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛)) ↔ ((𝑃‘𝑛) ∈ ℝ ∧ ∃𝑦 ∈ ℝ+
((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛))) |
31 | 23, 29, 30 | sylanbrc 586 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑦 ∈ ℝ+ ((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛))) |
32 | 31 | ralimi 3075 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
(1...𝑁)((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∀𝑛 ∈ (1...𝑁)∃𝑦 ∈ ℝ+ ((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛))) |
33 | | oveq2 7179 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (ℎ‘𝑛) → ((𝑃‘𝑛)(ball‘𝐷)𝑦) = ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛))) |
34 | 33 | sseq1d 3909 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (ℎ‘𝑛) → (((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛) ↔ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛))) |
35 | 34 | anbi2d 632 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (ℎ‘𝑛) → (((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛)) ↔ ((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛)))) |
36 | 35 | ac6sfi 8837 |
. . . . . . . . . . . . . . . 16
⊢
(((1...𝑁) ∈ Fin
∧ ∀𝑛 ∈
(1...𝑁)∃𝑦 ∈ ℝ+
((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛))) → ∃ℎ(ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛)))) |
37 | 2, 32, 36 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
(1...𝑁)((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃ℎ(ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛)))) |
38 | | 1rp 12477 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ+ |
39 | 38 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧
(1...𝑁) = ∅) → 1
∈ ℝ+) |
40 | | frn 6512 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ:(1...𝑁)⟶ℝ+ → ran
ℎ ⊆
ℝ+) |
41 | 40 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ ¬
(1...𝑁) = ∅) →
ran ℎ ⊆
ℝ+) |
42 | | ffn 6505 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ:(1...𝑁)⟶ℝ+ → ℎ Fn (1...𝑁)) |
43 | | fnfi 8779 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ Fn (1...𝑁) ∧ (1...𝑁) ∈ Fin) → ℎ ∈ Fin) |
44 | 42, 2, 43 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ:(1...𝑁)⟶ℝ+ → ℎ ∈ Fin) |
45 | | rnfi 8881 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ ∈ Fin → ran ℎ ∈ Fin) |
46 | 44, 45 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ:(1...𝑁)⟶ℝ+ → ran
ℎ ∈
Fin) |
47 | 46 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ ¬
(1...𝑁) = ∅) →
ran ℎ ∈
Fin) |
48 | | dm0rn0 5769 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (dom
ℎ = ∅ ↔ ran ℎ = ∅) |
49 | | fdm 6514 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ:(1...𝑁)⟶ℝ+ → dom
ℎ = (1...𝑁)) |
50 | 49 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ:(1...𝑁)⟶ℝ+ → (dom
ℎ = ∅ ↔
(1...𝑁) =
∅)) |
51 | 48, 50 | bitr3id 288 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ:(1...𝑁)⟶ℝ+ → (ran
ℎ = ∅ ↔
(1...𝑁) =
∅)) |
52 | 51 | necon3abid 2970 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ:(1...𝑁)⟶ℝ+ → (ran
ℎ ≠ ∅ ↔ ¬
(1...𝑁) =
∅)) |
53 | 52 | biimpar 481 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ ¬
(1...𝑁) = ∅) →
ran ℎ ≠
∅) |
54 | | rpssre 12480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
ℝ+ ⊆ ℝ |
55 | 40, 54 | sstrdi 3890 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ:(1...𝑁)⟶ℝ+ → ran
ℎ ⊆
ℝ) |
56 | 55 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ ¬
(1...𝑁) = ∅) →
ran ℎ ⊆
ℝ) |
57 | | ltso 10800 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ < Or
ℝ |
58 | | fiinfcl 9039 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (( <
Or ℝ ∧ (ran ℎ
∈ Fin ∧ ran ℎ ≠
∅ ∧ ran ℎ ⊆
ℝ)) → inf(ran ℎ,
ℝ, < ) ∈ ran ℎ) |
59 | 57, 58 | mpan 690 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((ran
ℎ ∈ Fin ∧ ran ℎ ≠ ∅ ∧ ran ℎ ⊆ ℝ) → inf(ran
ℎ, ℝ, < ) ∈
ran ℎ) |
60 | 47, 53, 56, 59 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ ¬
(1...𝑁) = ∅) →
inf(ran ℎ, ℝ, < )
∈ ran ℎ) |
61 | 41, 60 | sseldd 3879 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ ¬
(1...𝑁) = ∅) →
inf(ran ℎ, ℝ, < )
∈ ℝ+) |
62 | 39, 61 | ifclda 4450 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ:(1...𝑁)⟶ℝ+ →
if((1...𝑁) = ∅, 1,
inf(ran ℎ, ℝ, < ))
∈ ℝ+) |
63 | 62 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛))) → if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈
ℝ+) |
64 | 62 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈
ℝ+) |
65 | 64 | rpxrd 12516 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈
ℝ*) |
66 | | ffvelrn 6860 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → (ℎ‘𝑛) ∈
ℝ+) |
67 | 66 | rpxrd 12516 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → (ℎ‘𝑛) ∈
ℝ*) |
68 | | ne0i 4224 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ (1...𝑁) → (1...𝑁) ≠ ∅) |
69 | | ifnefalse 4427 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
((1...𝑁) ≠
∅ → if((1...𝑁) =
∅, 1, inf(ran ℎ,
ℝ, < )) = inf(ran ℎ, ℝ, < )) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑛 ∈ (1...𝑁) → if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) = inf(ran ℎ, ℝ, <
)) |
71 | 70 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) = inf(ran ℎ, ℝ, <
)) |
72 | 55 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → ran ℎ ⊆ ℝ) |
73 | | 0re 10722 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
ℝ |
74 | | rpge0 12486 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℝ+
→ 0 ≤ 𝑦) |
75 | 74 | rgen 3063 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
∀𝑦 ∈
ℝ+ 0 ≤ 𝑦 |
76 | | ssralv 3944 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ran
ℎ ⊆
ℝ+ → (∀𝑦 ∈ ℝ+ 0 ≤ 𝑦 → ∀𝑦 ∈ ran ℎ0 ≤ 𝑦)) |
77 | 40, 75, 76 | mpisyl 21 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ℎ:(1...𝑁)⟶ℝ+ →
∀𝑦 ∈ ran ℎ0 ≤ 𝑦) |
78 | | breq1 5034 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑦 ↔ 0 ≤ 𝑦)) |
79 | 78 | ralbidv 3109 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = 0 → (∀𝑦 ∈ ran ℎ 𝑥 ≤ 𝑦 ↔ ∀𝑦 ∈ ran ℎ0 ≤ 𝑦)) |
80 | 79 | rspcev 3527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((0
∈ ℝ ∧ ∀𝑦 ∈ ran ℎ0 ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ℎ 𝑥 ≤ 𝑦) |
81 | 73, 77, 80 | sylancr 590 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ:(1...𝑁)⟶ℝ+ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran ℎ 𝑥 ≤ 𝑦) |
82 | 81 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ℎ 𝑥 ≤ 𝑦) |
83 | | fnfvelrn 6859 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ℎ Fn (1...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → (ℎ‘𝑛) ∈ ran ℎ) |
84 | 42, 83 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → (ℎ‘𝑛) ∈ ran ℎ) |
85 | | infrelb 11704 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ran
ℎ ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran ℎ 𝑥 ≤ 𝑦 ∧ (ℎ‘𝑛) ∈ ran ℎ) → inf(ran ℎ, ℝ, < ) ≤ (ℎ‘𝑛)) |
86 | 72, 82, 84, 85 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → inf(ran ℎ, ℝ, < ) ≤ (ℎ‘𝑛)) |
87 | 71, 86 | eqbrtrd 5053 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ≤ (ℎ‘𝑛)) |
88 | 65, 67, 87 | jca31 518 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → ((if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈ ℝ*
∧ (ℎ‘𝑛) ∈ ℝ*)
∧ if((1...𝑁) = ∅,
1, inf(ran ℎ, ℝ, <
)) ≤ (ℎ‘𝑛))) |
89 | | ssbl 23177 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐷 ∈
(∞Met‘ℝ) ∧ (𝑃‘𝑛) ∈ ℝ) ∧ (if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈
ℝ* ∧ (ℎ‘𝑛) ∈ ℝ*) ∧
if((1...𝑁) = ∅, 1,
inf(ran ℎ, ℝ, < ))
≤ (ℎ‘𝑛)) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛))) |
90 | 89 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐷 ∈
(∞Met‘ℝ) ∧ (𝑃‘𝑛) ∈ ℝ) ∧ ((if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈
ℝ* ∧ (ℎ‘𝑛) ∈ ℝ*) ∧
if((1...𝑁) = ∅, 1,
inf(ran ℎ, ℝ, < ))
≤ (ℎ‘𝑛))) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛))) |
91 | 25, 90 | mpanl1 700 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑃‘𝑛) ∈ ℝ ∧ ((if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈
ℝ* ∧ (ℎ‘𝑛) ∈ ℝ*) ∧
if((1...𝑁) = ∅, 1,
inf(ran ℎ, ℝ, < ))
≤ (ℎ‘𝑛))) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛))) |
92 | 91 | ancoms 462 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((if((1...𝑁) =
∅, 1, inf(ran ℎ,
ℝ, < )) ∈ ℝ* ∧ (ℎ‘𝑛) ∈ ℝ*) ∧
if((1...𝑁) = ∅, 1,
inf(ran ℎ, ℝ, < ))
≤ (ℎ‘𝑛)) ∧ (𝑃‘𝑛) ∈ ℝ) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛))) |
93 | 88, 92 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑃‘𝑛) ∈ ℝ) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛))) |
94 | | sstr2 3885 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) → (((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛))) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑃‘𝑛) ∈ ℝ) → (((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛))) |
96 | 95 | expimpd 457 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → (((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛)) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛))) |
97 | 96 | ralimdva 3091 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ:(1...𝑁)⟶ℝ+ →
(∀𝑛 ∈
(1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛)) → ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛))) |
98 | 97 | imp 410 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛))) → ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛)) |
99 | 24 | fveq2i 6678 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(ball‘𝐷) =
(ball‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) |
100 | 99 | oveqi 7184 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) = ((𝑃‘𝑛)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) |
101 | 100 | sseq1i 3906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛) ↔ ((𝑃‘𝑛)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛)) |
102 | 101 | ralbii 3080 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛)) |
103 | | nfv 1920 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑑∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛) |
104 | 102, 103 | nfxfr 1859 |
. . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑑∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛) |
105 | | oveq2 7179 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) → ((𝑃‘𝑛)(ball‘𝐷)𝑑) = ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )))) |
106 | 105 | sseq1d 3909 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) → (((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛) ↔ ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛))) |
107 | 106 | ralbidv 3109 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) → (∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛))) |
108 | 104, 107 | rspce 3516 |
. . . . . . . . . . . . . . . . 17
⊢
((if((1...𝑁) =
∅, 1, inf(ran ℎ,
ℝ, < )) ∈ ℝ+ ∧ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛)) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) |
109 | 63, 98, 108 | syl2anc 587 |
. . . . . . . . . . . . . . . 16
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛))) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) |
110 | 109 | exlimiv 1936 |
. . . . . . . . . . . . . . 15
⊢
(∃ℎ(ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛))) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) |
111 | 37, 110 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(∀𝑛 ∈
(1...𝑁)((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) |
112 | 19, 111 | sylbir 238 |
. . . . . . . . . . . . 13
⊢
((∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧
∀𝑛 ∈ (1...𝑁)(𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) |
113 | 18, 112 | sylan2 596 |
. . . . . . . . . . . 12
⊢
((∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ 𝑃 ∈ X𝑛 ∈
(1...𝑁)(𝑔‘𝑛)) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) |
114 | 16, 113 | sylanb 584 |
. . . . . . . . . . 11
⊢
((∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧ 𝑃 ∈ X𝑛 ∈
(1...𝑁)(𝑔‘𝑛)) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) |
115 | | sstr2 3885 |
. . . . . . . . . . . . 13
⊢ (X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) → (X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ⊆ 𝑆 → X𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) |
116 | | ss2ixp 8521 |
. . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛) → X𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛)) |
117 | 115, 116 | syl11 33 |
. . . . . . . . . . . 12
⊢ (X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ⊆ 𝑆 → (∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛) → X𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) |
118 | 117 | reximdv 3183 |
. . . . . . . . . . 11
⊢ (X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ⊆ 𝑆 → (∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) |
119 | 114, 118 | syl5com 31 |
. . . . . . . . . 10
⊢
((∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧ 𝑃 ∈ X𝑛 ∈
(1...𝑁)(𝑔‘𝑛)) → (X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ⊆ 𝑆 → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) |
120 | 119 | expimpd 457 |
. . . . . . . . 9
⊢
(∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) →
((𝑃 ∈ X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∧ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) |
121 | | eleq2 2821 |
. . . . . . . . . . 11
⊢ (𝑧 = X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛))) |
122 | | sseq1 3903 |
. . . . . . . . . . 11
⊢ (𝑧 = X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) → (𝑧 ⊆ 𝑆 ↔ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ⊆ 𝑆)) |
123 | 121, 122 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑧 = X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) ↔ (𝑃 ∈ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∧ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ⊆ 𝑆))) |
124 | 123 | imbi1d 345 |
. . . . . . . . 9
⊢ (𝑧 = X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) → (((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆) ↔ ((𝑃 ∈ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∧ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆))) |
125 | 120, 124 | syl5ibrcom 250 |
. . . . . . . 8
⊢
(∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) →
(𝑧 = X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆))) |
126 | 125 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝑔 Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑧 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑧)(𝑔‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) →
(𝑧 = X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆))) |
127 | 126 | imp 410 |
. . . . . 6
⊢ (((𝑔 Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑧 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑧)(𝑔‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑧 = X𝑛 ∈
(1...𝑁)(𝑔‘𝑛)) → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) |
128 | 127 | exlimiv 1936 |
. . . . 5
⊢
(∃𝑔((𝑔 Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑧 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑧)(𝑔‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑧 = X𝑛 ∈
(1...𝑁)(𝑔‘𝑛)) → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) |
129 | 12, 128 | sylbi 220 |
. . . 4
⊢ (𝑧 ∈ {𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))} → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) |
130 | 129 | rexlimiv 3190 |
. . 3
⊢
(∃𝑧 ∈
{𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))} (𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆) |
131 | 11, 130 | syl 17 |
. 2
⊢ ((𝑆 ∈ (topGen‘{𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))}) ∧ 𝑃 ∈ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆) |
132 | 10, 131 | sylanb 584 |
1
⊢ ((𝑆 ∈ 𝑅 ∧ 𝑃 ∈ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆) |