This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Metamath Proof Explorer
Description: Lemma 2 for 0wlkon and 0trlon . (Contributed by AV, 3-Jan-2021)
(Revised by AV, 23-Mar-2021)
|
|
Ref |
Expression |
|
Hypothesis |
0wlk.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
|
Assertion |
0wlkonlem2 |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑃 ∈ ( 𝑉 ↑pm ( 0 ... 0 ) ) ) |
Proof
| Step |
Hyp |
Ref |
Expression |
| 1 |
|
0wlk.v |
⊢ 𝑉 = ( Vtx ‘ 𝐺 ) |
| 2 |
|
ovex |
⊢ ( 0 ... 0 ) ∈ V |
| 3 |
1
|
fvexi |
⊢ 𝑉 ∈ V |
| 4 |
|
simpl |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) |
| 5 |
|
fpmg |
⊢ ( ( ( 0 ... 0 ) ∈ V ∧ 𝑉 ∈ V ∧ 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ) → 𝑃 ∈ ( 𝑉 ↑pm ( 0 ... 0 ) ) ) |
| 6 |
2 3 4 5
|
mp3an12i |
⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑃 ∈ ( 𝑉 ↑pm ( 0 ... 0 ) ) ) |