Metamath Proof Explorer


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=VtxG
Assertion 0wlkonlem2 P:00VP0=NPV𝑝𝑚00

Proof

Step Hyp Ref Expression
1 0wlk.v V=VtxG
2 ovex 00V
3 1 fvexi VV
4 simpl P:00VP0=NP:00V
5 fpmg 00VVVP:00VPV𝑝𝑚00
6 2 3 4 5 mp3an12i P:00VP0=NPV𝑝𝑚00