Metamath Proof Explorer

Theorem wwlksnexthasheq

Description: The number of the extensions of a walk (as word) by an edge equals the number of vertices being connected to the trailing vertex of the walk. (Contributed by Alexander van der Vekens, 23-Aug-2018) (Revised by AV, 19-Apr-2021) (Revised by AV, 27-Oct-2022)

Ref Expression
Hypotheses wwlksnexthasheq.v ⊢ V = Vtx ⁡ G
wwlksnexthasheq.e ⊢ E = Edg ⁡ G
Assertion wwlksnexthasheq ⊢ W ∈ N WWalksN G → w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E = n ∈ V | lastS ⁡ W n ∈ E

Proof

Step Hyp Ref Expression
1 wwlksnexthasheq.v ⊢ V = Vtx ⁡ G
2 wwlksnexthasheq.e ⊢ E = Edg ⁡ G
3 ovex ⊢ N + 1 WWalksN G ∈ V
4 3 rabex ⊢ w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ∈ V
5 1 2 wwlksnextbij ⊢ W ∈ N WWalksN G → ∃ f f : w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ⟶ 1-1 onto n ∈ V | lastS ⁡ W n ∈ E
6 hasheqf1oi ⊢ w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ∈ V → ∃ f f : w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E ⟶ 1-1 onto n ∈ V | lastS ⁡ W n ∈ E → w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E = n ∈ V | lastS ⁡ W n ∈ E
7 4 5 6 mpsyl ⊢ W ∈ N WWalksN G → w ∈ N + 1 WWalksN G | w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E = n ∈ V | lastS ⁡ W n ∈ E