This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 0wlkonlem1

Description: Lemma 1 for 0wlkon and 0trlon . (Contributed by AV, 3-Jan-2021) (Revised by AV, 23-Mar-2021)

Ref Expression
Hypothesis 0wlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
Assertion 0wlkonlem1 ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )

Proof

Step Hyp Ref Expression
1 0wlk.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 id ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 )
3 0nn0 ⊢ 0 ∈ ℕ0
4 0elfz ⊢ ( 0 ∈ ℕ0 → 0 ∈ ( 0 ... 0 ) )
5 3 4 mp1i ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → 0 ∈ ( 0 ... 0 ) )
6 2 5 ffvelcdmd ⊢ ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
7 6 adantr ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑃 ‘ 0 ) ∈ 𝑉 )
8 eleq1 ⊢ ( 𝑁 = ( 𝑃 ‘ 0 ) → ( 𝑁 ∈ 𝑉 ↔ ( 𝑃 ‘ 0 ) ∈ 𝑉 ) )
9 8 eqcoms ⊢ ( ( 𝑃 ‘ 0 ) = 𝑁 → ( 𝑁 ∈ 𝑉 ↔ ( 𝑃 ‘ 0 ) ∈ 𝑉 ) )
10 9 adantl ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑁 ∈ 𝑉 ↔ ( 𝑃 ‘ 0 ) ∈ 𝑉 ) )
11 7 10 mpbird ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → 𝑁 ∈ 𝑉 )
12 id ⊢ ( 𝑁 ∈ 𝑉 → 𝑁 ∈ 𝑉 )
13 11 12 jccir ⊢ ( ( 𝑃 : ( 0 ... 0 ) ⟶ 𝑉 ∧ ( 𝑃 ‘ 0 ) = 𝑁 ) → ( 𝑁 ∈ 𝑉 ∧ 𝑁 ∈ 𝑉 ) )