Step |
Hyp |
Ref |
Expression |
0 |
|
chli |
⊢ ⇝𝑣 |
1 |
|
vf |
⊢ 𝑓 |
2 |
|
vw |
⊢ 𝑤 |
3 |
1
|
cv |
⊢ 𝑓 |
4 |
|
cn |
⊢ ℕ |
5 |
|
chba |
⊢ ℋ |
6 |
4 5 3
|
wf |
⊢ 𝑓 : ℕ ⟶ ℋ |
7 |
2
|
cv |
⊢ 𝑤 |
8 |
7 5
|
wcel |
⊢ 𝑤 ∈ ℋ |
9 |
6 8
|
wa |
⊢ ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) |
10 |
|
vx |
⊢ 𝑥 |
11 |
|
crp |
⊢ ℝ+ |
12 |
|
vy |
⊢ 𝑦 |
13 |
|
vz |
⊢ 𝑧 |
14 |
|
cuz |
⊢ ℤ≥ |
15 |
12
|
cv |
⊢ 𝑦 |
16 |
15 14
|
cfv |
⊢ ( ℤ≥ ‘ 𝑦 ) |
17 |
|
cno |
⊢ normℎ |
18 |
13
|
cv |
⊢ 𝑧 |
19 |
18 3
|
cfv |
⊢ ( 𝑓 ‘ 𝑧 ) |
20 |
|
cmv |
⊢ −ℎ |
21 |
19 7 20
|
co |
⊢ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) |
22 |
21 17
|
cfv |
⊢ ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) |
23 |
|
clt |
⊢ < |
24 |
10
|
cv |
⊢ 𝑥 |
25 |
22 24 23
|
wbr |
⊢ ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 |
26 |
25 13 16
|
wral |
⊢ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 |
27 |
26 12 4
|
wrex |
⊢ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 |
28 |
27 10 11
|
wral |
⊢ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 |
29 |
9 28
|
wa |
⊢ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) |
30 |
29 1 2
|
copab |
⊢ { 〈 𝑓 , 𝑤 〉 ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) } |
31 |
0 30
|
wceq |
⊢ ⇝𝑣 = { 〈 𝑓 , 𝑤 〉 ∣ ( ( 𝑓 : ℕ ⟶ ℋ ∧ 𝑤 ∈ ℋ ) ∧ ∀ 𝑥 ∈ ℝ+ ∃ 𝑦 ∈ ℕ ∀ 𝑧 ∈ ( ℤ≥ ‘ 𝑦 ) ( normℎ ‘ ( ( 𝑓 ‘ 𝑧 ) −ℎ 𝑤 ) ) < 𝑥 ) } |