Theorem 0wlkonlem2

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 ) ) )