Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
⊢ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 = 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 |
2 |
|
eqid |
⊢ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) = ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) |
3 |
1 2
|
hhxmet |
⊢ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ∈ ( ∞Met ‘ ℋ ) |
4 |
|
eqid |
⊢ ( MetOpen ‘ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ) = ( MetOpen ‘ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ) |
5 |
4
|
methaus |
⊢ ( ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ∈ ( ∞Met ‘ ℋ ) → ( MetOpen ‘ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ) ∈ Haus ) |
6 |
|
lmfun |
⊢ ( ( MetOpen ‘ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ) ∈ Haus → Fun ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ) ) ) |
7 |
3 5 6
|
mp2b |
⊢ Fun ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ) ) |
8 |
|
funres |
⊢ ( Fun ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ) ) → Fun ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ) ) ↾ ( ℋ ↑m ℕ ) ) ) |
9 |
7 8
|
ax-mp |
⊢ Fun ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ) ) ↾ ( ℋ ↑m ℕ ) ) |
10 |
1 2 4
|
hhlm |
⊢ ⇝𝑣 = ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ) ) ↾ ( ℋ ↑m ℕ ) ) |
11 |
10
|
funeqi |
⊢ ( Fun ⇝𝑣 ↔ Fun ( ( ⇝𝑡 ‘ ( MetOpen ‘ ( IndMet ‘ 〈 〈 +ℎ , ·ℎ 〉 , normℎ 〉 ) ) ) ↾ ( ℋ ↑m ℕ ) ) ) |
12 |
9 11
|
mpbir |
⊢ Fun ⇝𝑣 |
13 |
|
funfn |
⊢ ( Fun ⇝𝑣 ↔ ⇝𝑣 Fn dom ⇝𝑣 ) |
14 |
12 13
|
mpbi |
⊢ ⇝𝑣 Fn dom ⇝𝑣 |
15 |
|
funfvbrb |
⊢ ( Fun ⇝𝑣 → ( 𝑥 ∈ dom ⇝𝑣 ↔ 𝑥 ⇝𝑣 ( ⇝𝑣 ‘ 𝑥 ) ) ) |
16 |
12 15
|
ax-mp |
⊢ ( 𝑥 ∈ dom ⇝𝑣 ↔ 𝑥 ⇝𝑣 ( ⇝𝑣 ‘ 𝑥 ) ) |
17 |
|
fvex |
⊢ ( ⇝𝑣 ‘ 𝑥 ) ∈ V |
18 |
17
|
hlimveci |
⊢ ( 𝑥 ⇝𝑣 ( ⇝𝑣 ‘ 𝑥 ) → ( ⇝𝑣 ‘ 𝑥 ) ∈ ℋ ) |
19 |
16 18
|
sylbi |
⊢ ( 𝑥 ∈ dom ⇝𝑣 → ( ⇝𝑣 ‘ 𝑥 ) ∈ ℋ ) |
20 |
19
|
rgen |
⊢ ∀ 𝑥 ∈ dom ⇝𝑣 ( ⇝𝑣 ‘ 𝑥 ) ∈ ℋ |
21 |
|
ffnfv |
⊢ ( ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ ↔ ( ⇝𝑣 Fn dom ⇝𝑣 ∧ ∀ 𝑥 ∈ dom ⇝𝑣 ( ⇝𝑣 ‘ 𝑥 ) ∈ ℋ ) ) |
22 |
14 20 21
|
mpbir2an |
⊢ ⇝𝑣 : dom ⇝𝑣 ⟶ ℋ |