Metamath Proof Explorer

Theorem wwlksonvtx

Description: If a word W represents a walk of length 2 on two classes A and C , these classes are vertices. (Contributed by AV, 14-Mar-2022)

Ref Expression
Hypothesis wwlksonvtx.v ⊢V=Vtx⁡G
Assertion wwlksonvtx ⊢W∈ANWWalksNOnGC→A∈V∧C∈V

Proof

Step Hyp Ref Expression
1 wwlksonvtx.v ⊢V=Vtx⁡G
2 fvex ⊢Vtx⁡g∈V
3 2 2 pm3.2i ⊢Vtx⁡g∈V∧Vtx⁡g∈V
4 3 rgen2w ⊢∀n∈ℕ0∀g∈VVtx⁡g∈V∧Vtx⁡g∈V
5 df-wwlksnon ⊢WWalksNOn=n∈ℕ0,g∈V⟼a∈Vtx⁡g,b∈Vtx⁡g⟼w∈nWWalksNg|w⁡0=a∧w⁡n=b
6 fveq2 ⊢g=G→Vtx⁡g=Vtx⁡G
7 6 6 jca ⊢g=G→Vtx⁡g=Vtx⁡G∧Vtx⁡g=Vtx⁡G
8 7 adantl ⊢n=N∧g=G→Vtx⁡g=Vtx⁡G∧Vtx⁡g=Vtx⁡G
9 5 8 el2mpocl ⊢∀n∈ℕ0∀g∈VVtx⁡g∈V∧Vtx⁡g∈V→W∈ANWWalksNOnGC→N∈ℕ0∧G∈V∧A∈Vtx⁡G∧C∈Vtx⁡G
10 4 9 ax-mp ⊢W∈ANWWalksNOnGC→N∈ℕ0∧G∈V∧A∈Vtx⁡G∧C∈Vtx⁡G
11 1 eleq2i ⊢A∈V↔A∈Vtx⁡G
12 1 eleq2i ⊢C∈V↔C∈Vtx⁡G
13 11 12 anbi12i ⊢A∈V∧C∈V↔A∈Vtx⁡G∧C∈Vtx⁡G
14 13 biimpri ⊢A∈Vtx⁡G∧C∈Vtx⁡G→A∈V∧C∈V
15 10 14 simpl2im ⊢W∈ANWWalksNOnGC→A∈V∧C∈V