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 ∈ A N WWalksNOn G C → 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 ∈ V Vtx ⁡ g ∈ V ∧ Vtx ⁡ g ∈ V
5 df-wwlksnon ⊢ WWalksNOn = n ∈ ℕ 0 , g ∈ V ⟼ a ∈ Vtx ⁡ g , b ∈ Vtx ⁡ g ⟼ w ∈ n WWalksN g | 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 ∈ V Vtx ⁡ g ∈ V ∧ Vtx ⁡ g ∈ V → W ∈ A N WWalksNOn G C → N ∈ ℕ 0 ∧ G ∈ V ∧ A ∈ Vtx ⁡ G ∧ C ∈ Vtx ⁡ G
10 4 9 ax-mp ⊢ W ∈ A N WWalksNOn G C → 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 ∈ A N WWalksNOn G C → A ∈ V ∧ C ∈ V