| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | ptrecube.r | . . . 4
⊢ 𝑅 =
(∏t‘((1...𝑁) × {(topGen‘ran
(,))})) | 
| 2 |  | fzfi 14014 | . . . . 5
⊢
(1...𝑁) ∈
Fin | 
| 3 |  | retop 24783 | . . . . . 6
⊢
(topGen‘ran (,)) ∈ Top | 
| 4 |  | fnconstg 6795 | . . . . . 6
⊢
((topGen‘ran (,)) ∈ Top → ((1...𝑁) × {(topGen‘ran (,))}) Fn
(1...𝑁)) | 
| 5 | 3, 4 | ax-mp 5 | . . . . 5
⊢
((1...𝑁) ×
{(topGen‘ran (,))}) Fn (1...𝑁) | 
| 6 |  | eqid 2736 | . . . . . 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 23579 | . . . . 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 2764 | . . 3
⊢ 𝑅 = (topGen‘{𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))}) | 
| 10 | 9 | eleq2i 2832 | . 2
⊢ (𝑆 ∈ 𝑅 ↔ 𝑆 ∈ (topGen‘{𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))})) | 
| 11 |  | tg2 22973 | . . 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 23581 | . . . . 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 6918 | . . . . . . . . . . . . . . 15
⊢
(topGen‘ran (,)) ∈ V | 
| 14 | 13 | fvconst2 7225 | . . . . . . . . . . . . . 14
⊢ (𝑛 ∈ (1...𝑁) → (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) =
(topGen‘ran (,))) | 
| 15 | 14 | eleq2d 2826 | . . . . . . . . . . . . 13
⊢ (𝑛 ∈ (1...𝑁) → ((𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ↔
(𝑔‘𝑛) ∈ (topGen‘ran
(,)))) | 
| 16 | 15 | ralbiia 3090 | . . . . . . . . . . . 12
⊢
(∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ↔
∀𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∈ (topGen‘ran
(,))) | 
| 17 |  | elixp2 8942 | . . . . . . . . . . . . . 14
⊢ (𝑃 ∈ X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ↔ (𝑃 ∈ V ∧ 𝑃 Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(𝑃‘𝑛) ∈ (𝑔‘𝑛))) | 
| 18 | 17 | simp3bi 1147 | . . . . . . . . . . . . 13
⊢ (𝑃 ∈ X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) → ∀𝑛 ∈ (1...𝑁)(𝑃‘𝑛) ∈ (𝑔‘𝑛)) | 
| 19 |  | r19.26 3110 | . . . . . . . . . . . . . 14
⊢
(∀𝑛 ∈
(1...𝑁)((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) ↔ (∀𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧
∀𝑛 ∈ (1...𝑁)(𝑃‘𝑛) ∈ (𝑔‘𝑛))) | 
| 20 |  | uniretop 24784 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ℝ =
∪ (topGen‘ran (,)) | 
| 21 | 20 | eltopss 22914 | . . . . . . . . . . . . . . . . . . . 20
⊢
(((topGen‘ran (,)) ∈ Top ∧ (𝑔‘𝑛) ∈ (topGen‘ran (,))) →
(𝑔‘𝑛) ⊆ ℝ) | 
| 22 | 3, 21 | mpan 690 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑔‘𝑛) ∈ (topGen‘ran (,)) → (𝑔‘𝑛) ⊆ ℝ) | 
| 23 | 22 | sselda 3982 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → (𝑃‘𝑛) ∈ ℝ) | 
| 24 |  | ptrecube.d | . . . . . . . . . . . . . . . . . . . 20
⊢ 𝐷 = ((abs ∘ − )
↾ (ℝ × ℝ)) | 
| 25 | 24 | rexmet 24813 | . . . . . . . . . . . . . . . . . . 19
⊢ 𝐷 ∈
(∞Met‘ℝ) | 
| 26 |  | eqid 2736 | . . . . . . . . . . . . . . . . . . . . 21
⊢
(MetOpen‘𝐷) =
(MetOpen‘𝐷) | 
| 27 | 24, 26 | tgioo 24818 | . . . . . . . . . . . . . . . . . . . 20
⊢
(topGen‘ran (,)) = (MetOpen‘𝐷) | 
| 28 | 27 | mopni2 24507 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝐷 ∈
(∞Met‘ℝ) ∧ (𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑦 ∈ ℝ+ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛)) | 
| 29 | 25, 28 | mp3an1 1449 | . . . . . . . . . . . . . . . . . 18
⊢ (((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑦 ∈ ℝ+ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛)) | 
| 30 |  | r19.42v 3190 | . . . . . . . . . . . . . . . . . 18
⊢
(∃𝑦 ∈
ℝ+ ((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛)) ↔ ((𝑃‘𝑛) ∈ ℝ ∧ ∃𝑦 ∈ ℝ+
((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛))) | 
| 31 | 23, 29, 30 | sylanbrc 583 | . . . . . . . . . . . . . . . . 17
⊢ (((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑦 ∈ ℝ+ ((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛))) | 
| 32 | 31 | ralimi 3082 | . . . . . . . . . . . . . . . 16
⊢
(∀𝑛 ∈
(1...𝑁)((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∀𝑛 ∈ (1...𝑁)∃𝑦 ∈ ℝ+ ((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛))) | 
| 33 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (ℎ‘𝑛) → ((𝑃‘𝑛)(ball‘𝐷)𝑦) = ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛))) | 
| 34 | 33 | sseq1d 4014 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (ℎ‘𝑛) → (((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛) ↔ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛))) | 
| 35 | 34 | anbi2d 630 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (ℎ‘𝑛) → (((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛)) ↔ ((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛)))) | 
| 36 | 35 | ac6sfi 9321 | . . . . . . . . . . . . . . . 16
⊢
(((1...𝑁) ∈ Fin
∧ ∀𝑛 ∈
(1...𝑁)∃𝑦 ∈ ℝ+
((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)𝑦) ⊆ (𝑔‘𝑛))) → ∃ℎ(ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛)))) | 
| 37 | 2, 32, 36 | sylancr 587 | . . . . . . . . . . . . . . 15
⊢
(∀𝑛 ∈
(1...𝑁)((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃ℎ(ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛)))) | 
| 38 |  | 1rp 13039 | . . . . . . . . . . . . . . . . . . . 20
⊢ 1 ∈
ℝ+ | 
| 39 | 38 | a1i 11 | . . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧
(1...𝑁) = ∅) → 1
∈ ℝ+) | 
| 40 |  | frn 6742 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (ℎ:(1...𝑁)⟶ℝ+ → ran
ℎ ⊆
ℝ+) | 
| 41 | 40 | adantr 480 | . . . . . . . . . . . . . . . . . . . 20
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ ¬
(1...𝑁) = ∅) →
ran ℎ ⊆
ℝ+) | 
| 42 |  | ffn 6735 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ:(1...𝑁)⟶ℝ+ → ℎ Fn (1...𝑁)) | 
| 43 |  | fnfi 9219 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ Fn (1...𝑁) ∧ (1...𝑁) ∈ Fin) → ℎ ∈ Fin) | 
| 44 | 42, 2, 43 | sylancl 586 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ:(1...𝑁)⟶ℝ+ → ℎ ∈ Fin) | 
| 45 |  | rnfi 9381 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ ∈ Fin → ran ℎ ∈ Fin) | 
| 46 | 44, 45 | syl 17 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ:(1...𝑁)⟶ℝ+ → ran
ℎ ∈
Fin) | 
| 47 | 46 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ ¬
(1...𝑁) = ∅) →
ran ℎ ∈
Fin) | 
| 48 |  | dm0rn0 5934 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (dom
ℎ = ∅ ↔ ran ℎ = ∅) | 
| 49 |  | fdm 6744 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (ℎ:(1...𝑁)⟶ℝ+ → dom
ℎ = (1...𝑁)) | 
| 50 | 49 | eqeq1d 2738 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (ℎ:(1...𝑁)⟶ℝ+ → (dom
ℎ = ∅ ↔
(1...𝑁) =
∅)) | 
| 51 | 48, 50 | bitr3id 285 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ (ℎ:(1...𝑁)⟶ℝ+ → (ran
ℎ = ∅ ↔
(1...𝑁) =
∅)) | 
| 52 | 51 | necon3abid 2976 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ:(1...𝑁)⟶ℝ+ → (ran
ℎ ≠ ∅ ↔ ¬
(1...𝑁) =
∅)) | 
| 53 | 52 | biimpar 477 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ ¬
(1...𝑁) = ∅) →
ran ℎ ≠
∅) | 
| 54 |  | rpssre 13043 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢
ℝ+ ⊆ ℝ | 
| 55 | 40, 54 | sstrdi 3995 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ (ℎ:(1...𝑁)⟶ℝ+ → ran
ℎ ⊆
ℝ) | 
| 56 | 55 | adantr 480 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ ¬
(1...𝑁) = ∅) →
ran ℎ ⊆
ℝ) | 
| 57 |  | ltso 11342 | . . . . . . . . . . . . . . . . . . . . . 22
⊢  < Or
ℝ | 
| 58 |  | fiinfcl 9542 | . . . . . . . . . . . . . . . . . . . . . 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 3983 | . . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ ¬
(1...𝑁) = ∅) →
inf(ran ℎ, ℝ, < )
∈ ℝ+) | 
| 62 | 39, 61 | ifclda 4560 | . . . . . . . . . . . . . . . . . 18
⊢ (ℎ:(1...𝑁)⟶ℝ+ →
if((1...𝑁) = ∅, 1,
inf(ran ℎ, ℝ, < ))
∈ ℝ+) | 
| 63 | 62 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛))) → if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈
ℝ+) | 
| 64 | 62 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈
ℝ+) | 
| 65 | 64 | rpxrd 13079 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈
ℝ*) | 
| 66 |  | ffvelcdm 7100 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → (ℎ‘𝑛) ∈
ℝ+) | 
| 67 | 66 | rpxrd 13079 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → (ℎ‘𝑛) ∈
ℝ*) | 
| 68 |  | ne0i 4340 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑛 ∈ (1...𝑁) → (1...𝑁) ≠ ∅) | 
| 69 |  | ifnefalse 4536 | . . . . . . . . . . . . . . . . . . . . . . . . . 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 481 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) = inf(ran ℎ, ℝ, <
)) | 
| 72 | 55 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → ran ℎ ⊆ ℝ) | 
| 73 |  | 0re 11264 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ 0 ∈
ℝ | 
| 74 |  | rpge0 13049 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑦 ∈ ℝ+
→ 0 ≤ 𝑦) | 
| 75 | 74 | rgen 3062 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
∀𝑦 ∈
ℝ+ 0 ≤ 𝑦 | 
| 76 |  | ssralv 4051 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (ran
ℎ ⊆
ℝ+ → (∀𝑦 ∈ ℝ+ 0 ≤ 𝑦 → ∀𝑦 ∈ ran ℎ0 ≤ 𝑦)) | 
| 77 | 40, 75, 76 | mpisyl 21 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ℎ:(1...𝑁)⟶ℝ+ →
∀𝑦 ∈ ran ℎ0 ≤ 𝑦) | 
| 78 |  | breq1 5145 | . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑥 = 0 → (𝑥 ≤ 𝑦 ↔ 0 ≤ 𝑦)) | 
| 79 | 78 | ralbidv 3177 | . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑥 = 0 → (∀𝑦 ∈ ran ℎ 𝑥 ≤ 𝑦 ↔ ∀𝑦 ∈ ran ℎ0 ≤ 𝑦)) | 
| 80 | 79 | rspcev 3621 | . . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((0
∈ ℝ ∧ ∀𝑦 ∈ ran ℎ0 ≤ 𝑦) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ℎ 𝑥 ≤ 𝑦) | 
| 81 | 73, 77, 80 | sylancr 587 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (ℎ:(1...𝑁)⟶ℝ+ →
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran ℎ 𝑥 ≤ 𝑦) | 
| 82 | 81 | adantr 480 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ ran ℎ 𝑥 ≤ 𝑦) | 
| 83 |  | fnfvelrn 7099 | . . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((ℎ Fn (1...𝑁) ∧ 𝑛 ∈ (1...𝑁)) → (ℎ‘𝑛) ∈ ran ℎ) | 
| 84 | 42, 83 | sylan 580 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → (ℎ‘𝑛) ∈ ran ℎ) | 
| 85 |  | infrelb 12254 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((ran
ℎ ⊆ ℝ ∧
∃𝑥 ∈ ℝ
∀𝑦 ∈ ran ℎ 𝑥 ≤ 𝑦 ∧ (ℎ‘𝑛) ∈ ran ℎ) → inf(ran ℎ, ℝ, < ) ≤ (ℎ‘𝑛)) | 
| 86 | 72, 82, 84, 85 | syl3anc 1372 | . . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → inf(ran ℎ, ℝ, < ) ≤ (ℎ‘𝑛)) | 
| 87 | 71, 86 | eqbrtrd 5164 | . . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ≤ (ℎ‘𝑛)) | 
| 88 | 65, 67, 87 | jca31 514 | . . . . . . . . . . . . . . . . . . . . . 22
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → ((if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈ ℝ*
∧ (ℎ‘𝑛) ∈ ℝ*)
∧ if((1...𝑁) = ∅,
1, inf(ran ℎ, ℝ, <
)) ≤ (ℎ‘𝑛))) | 
| 89 |  | ssbl 24434 | . . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐷 ∈
(∞Met‘ℝ) ∧ (𝑃‘𝑛) ∈ ℝ) ∧ (if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) ∈
ℝ* ∧ (ℎ‘𝑛) ∈ ℝ*) ∧
if((1...𝑁) = ∅, 1,
inf(ran ℎ, ℝ, < ))
≤ (ℎ‘𝑛)) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛))) | 
| 90 | 89 | 3expb 1120 | . . . . . . . . . . . . . . . . . . . . . . . 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 458 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
((((if((1...𝑁) =
∅, 1, inf(ran ℎ,
ℝ, < )) ∈ ℝ* ∧ (ℎ‘𝑛) ∈ ℝ*) ∧
if((1...𝑁) = ∅, 1,
inf(ran ℎ, ℝ, < ))
≤ (ℎ‘𝑛)) ∧ (𝑃‘𝑛) ∈ ℝ) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛))) | 
| 93 | 88, 92 | sylan 580 | . . . . . . . . . . . . . . . . . . . . 21
⊢ (((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) ∧ (𝑃‘𝑛) ∈ ℝ) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛))) | 
| 94 |  | sstr2 3989 | . . . . . . . . . . . . . . . . . . . . 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 453 | . . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧ 𝑛 ∈ (1...𝑁)) → (((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛)) → ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛))) | 
| 97 | 96 | ralimdva 3166 | . . . . . . . . . . . . . . . . . 18
⊢ (ℎ:(1...𝑁)⟶ℝ+ →
(∀𝑛 ∈
(1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛)) → ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛))) | 
| 98 | 97 | imp 406 | . . . . . . . . . . . . . . . . 17
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛))) → ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛)) | 
| 99 | 24 | fveq2i 6908 | . . . . . . . . . . . . . . . . . . . . . 22
⊢
(ball‘𝐷) =
(ball‘((abs ∘ − ) ↾ (ℝ ×
ℝ))) | 
| 100 | 99 | oveqi 7445 | . . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) = ((𝑃‘𝑛)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) | 
| 101 | 100 | sseq1i 4011 | . . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛) ↔ ((𝑃‘𝑛)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛)) | 
| 102 | 101 | ralbii 3092 | . . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛)) | 
| 103 |  | nfv 1913 | . . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑑∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘((abs ∘ − ) ↾
(ℝ × ℝ)))if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛) | 
| 104 | 102, 103 | nfxfr 1852 | . . . . . . . . . . . . . . . . . 18
⊢
Ⅎ𝑑∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛) | 
| 105 |  | oveq2 7440 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑑 = if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) → ((𝑃‘𝑛)(ball‘𝐷)𝑑) = ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )))) | 
| 106 | 105 | sseq1d 4014 | . . . . . . . . . . . . . . . . . . 19
⊢ (𝑑 = if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) → (((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛) ↔ ((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛))) | 
| 107 | 106 | ralbidv 3177 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑑 = if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < )) → (∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛) ↔ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛))) | 
| 108 | 104, 107 | rspce 3610 | . . . . . . . . . . . . . . . . 17
⊢
((if((1...𝑁) =
∅, 1, inf(ran ℎ,
ℝ, < )) ∈ ℝ+ ∧ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)if((1...𝑁) = ∅, 1, inf(ran ℎ, ℝ, < ))) ⊆ (𝑔‘𝑛)) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) | 
| 109 | 63, 98, 108 | syl2anc 584 | . . . . . . . . . . . . . . . 16
⊢ ((ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛))) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) | 
| 110 | 109 | exlimiv 1929 | . . . . . . . . . . . . . . 15
⊢
(∃ℎ(ℎ:(1...𝑁)⟶ℝ+ ∧
∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛) ∈ ℝ ∧ ((𝑃‘𝑛)(ball‘𝐷)(ℎ‘𝑛)) ⊆ (𝑔‘𝑛))) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) | 
| 111 | 37, 110 | syl 17 | . . . . . . . . . . . . . 14
⊢
(∀𝑛 ∈
(1...𝑁)((𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ (𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) | 
| 112 | 19, 111 | sylbir 235 | . . . . . . . . . . . . 13
⊢
((∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧
∀𝑛 ∈ (1...𝑁)(𝑃‘𝑛) ∈ (𝑔‘𝑛)) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) | 
| 113 | 18, 112 | sylan2 593 | . . . . . . . . . . . 12
⊢
((∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (topGen‘ran (,)) ∧ 𝑃 ∈ X𝑛 ∈
(1...𝑁)(𝑔‘𝑛)) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) | 
| 114 | 16, 113 | sylanb 581 | . . . . . . . . . . 11
⊢
((∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧ 𝑃 ∈ X𝑛 ∈
(1...𝑁)(𝑔‘𝑛)) → ∃𝑑 ∈ ℝ+ ∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛)) | 
| 115 |  | sstr2 3989 | . . . . . . . . . . . . 13
⊢ (X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) → (X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ⊆ 𝑆 → X𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) | 
| 116 |  | ss2ixp 8951 | . . . . . . . . . . . . 13
⊢
(∀𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛) → X𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛)) | 
| 117 | 115, 116 | syl11 33 | . . . . . . . . . . . 12
⊢ (X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ⊆ 𝑆 → (∀𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ (𝑔‘𝑛) → X𝑛 ∈ (1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) | 
| 118 | 117 | reximdv 3169 | . . . . . . . . . . 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 453 | . . . . . . . . 9
⊢
(∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) →
((𝑃 ∈ X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∧ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) | 
| 121 |  | eleq2 2829 | . . . . . . . . . . 11
⊢ (𝑧 = X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) → (𝑃 ∈ 𝑧 ↔ 𝑃 ∈ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛))) | 
| 122 |  | sseq1 4008 | . . . . . . . . . . 11
⊢ (𝑧 = X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) → (𝑧 ⊆ 𝑆 ↔ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ⊆ 𝑆)) | 
| 123 | 121, 122 | anbi12d 632 | . . . . . . . . . 10
⊢ (𝑧 = X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) ↔ (𝑃 ∈ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∧ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ⊆ 𝑆))) | 
| 124 | 123 | imbi1d 341 | . . . . . . . . 9
⊢ (𝑧 = X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) → (((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆) ↔ ((𝑃 ∈ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∧ X𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆))) | 
| 125 | 120, 124 | syl5ibrcom 247 | . . . . . . . 8
⊢
(∀𝑛 ∈
(1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) →
(𝑧 = X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆))) | 
| 126 | 125 | 3ad2ant2 1134 | . . . . . . 7
⊢ ((𝑔 Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑧 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑧)(𝑔‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) →
(𝑧 = X𝑛 ∈
(1...𝑁)(𝑔‘𝑛) → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆))) | 
| 127 | 126 | imp 406 | . . . . . 6
⊢ (((𝑔 Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑧 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑧)(𝑔‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑧 = X𝑛 ∈
(1...𝑁)(𝑔‘𝑛)) → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) | 
| 128 | 127 | exlimiv 1929 | . . . . 5
⊢
(∃𝑔((𝑔 Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(𝑔‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑧 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑧)(𝑔‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑧 = X𝑛 ∈
(1...𝑁)(𝑔‘𝑛)) → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) | 
| 129 | 12, 128 | sylbi 217 | . . . 4
⊢ (𝑧 ∈ {𝑥 ∣ ∃ℎ((ℎ Fn (1...𝑁) ∧ ∀𝑛 ∈ (1...𝑁)(ℎ‘𝑛) ∈ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛) ∧
∃𝑤 ∈ Fin
∀𝑛 ∈
((1...𝑁) ∖ 𝑤)(ℎ‘𝑛) = ∪ (((1...𝑁) × {(topGen‘ran
(,))})‘𝑛)) ∧
𝑥 = X𝑛 ∈
(1...𝑁)(ℎ‘𝑛))} → ((𝑃 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆)) | 
| 130 | 129 | rexlimiv 3147 | . . 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 581 | 1
⊢ ((𝑆 ∈ 𝑅 ∧ 𝑃 ∈ 𝑆) → ∃𝑑 ∈ ℝ+ X𝑛 ∈
(1...𝑁)((𝑃‘𝑛)(ball‘𝐷)𝑑) ⊆ 𝑆) |