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	$$⊢V=\mathrm{Vtx}\left(G\right)$$
Assertion	0wlkonlem2	$$⊢\left(P:\left(0\dots 0\right)⟶V\wedge P\left(0\right)=N\right)\to P\in \left(V{\uparrow }_{𝑝𝑚}\left(0\dots 0\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		0wlk.v	$$⊢V=\mathrm{Vtx}\left(G\right)$$
2		ovex	$$⊢\left(0\dots 0\right)\in \mathrm{V}$$
3	1	fvexi	$$⊢V\in \mathrm{V}$$
4		simpl	$$⊢\left(P:\left(0\dots 0\right)⟶V\wedge P\left(0\right)=N\right)\to P:\left(0\dots 0\right)⟶V$$
5		fpmg	$$⊢\left(\left(0\dots 0\right)\in \mathrm{V}\wedge V\in \mathrm{V}\wedge P:\left(0\dots 0\right)⟶V\right)\to P\in \left(V{\uparrow }_{𝑝𝑚}\left(0\dots 0\right)\right)$$
6	2 3 4 5	mp3an12i	$$⊢\left(P:\left(0\dots 0\right)⟶V\wedge P\left(0\right)=N\right)\to P\in \left(V{\uparrow }_{𝑝𝑚}\left(0\dots 0\right)\right)$$