Metamath Proof Explorer

Theorem wwlksnextbij0

Description: Lemma for wwlksnextbij . (Contributed by Alexander van der Vekens, 7-Aug-2018) (Revised by AV, 18-Apr-2021)

Ref Expression
Hypotheses wwlksnextbij0.v ⊢ V = Vtx ⁡ G
wwlksnextbij0.e ⊢ E = Edg ⁡ G
wwlksnextbij0.d ⊢ D = w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
wwlksnextbij0.r ⊢ R = n ∈ V | lastS ⁡ W n ∈ E
wwlksnextbij0.f ⊢ F = t ∈ D ⟼ lastS ⁡ t
Assertion wwlksnextbij0 ⊢ W ∈ N WWalksN G → F : D ⟶ 1-1 onto R

Proof

Step Hyp Ref Expression
1 wwlksnextbij0.v ⊢ V = Vtx ⁡ G
2 wwlksnextbij0.e ⊢ E = Edg ⁡ G
3 wwlksnextbij0.d ⊢ D = w ∈ Word V | w = N + 2 ∧ w prefix N + 1 = W ∧ lastS ⁡ W lastS ⁡ w ∈ E
4 wwlksnextbij0.r ⊢ R = n ∈ V | lastS ⁡ W n ∈ E
5 wwlksnextbij0.f ⊢ F = t ∈ D ⟼ lastS ⁡ t
6 1 wwlknbp ⊢ W ∈ N WWalksN G → G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V
7 1 2 3 4 5 wwlksnextinj ⊢ N ∈ ℕ 0 → F : D ⟶ 1-1 R
8 7 3ad2ant2 ⊢ G ∈ V ∧ N ∈ ℕ 0 ∧ W ∈ Word V → F : D ⟶ 1-1 R
9 6 8 syl ⊢ W ∈ N WWalksN G → F : D ⟶ 1-1 R
10 1 2 3 4 5 wwlksnextsurj ⊢ W ∈ N WWalksN G → F : D ⟶ onto R
11 df-f1o ⊢ F : D ⟶ 1-1 onto R ↔ F : D ⟶ 1-1 R ∧ F : D ⟶ onto R
12 9 10 11 sylanbrc ⊢ W ∈ N WWalksN G → F : D ⟶ 1-1 onto R