# Metamath Proof Explorer

## Theorem numclwwlk1lem2f1o

Description: T is a 1-1 onto function. (Contributed by Alexander van der Vekens, 26-Sep-2018) (Revised by AV, 29-May-2021) (Revised by AV, 6-Mar-2022)

Ref Expression
Hypotheses extwwlkfab.v $⊢ V = Vtx ⁡ G$
extwwlkfab.c $⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v$
extwwlkfab.f $⊢ F = X ClWWalksNOn ⁡ G N − 2$
numclwwlk.t $⊢ T = u ∈ X C N ⟼ u prefix N − 2 u ⁡ N − 1$
Assertion numclwwlk1lem2f1o $⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → T : X C N ⟶ 1-1 onto F × G NeighbVtx X$

### Proof

Step Hyp Ref Expression
1 extwwlkfab.v $⊢ V = Vtx ⁡ G$
2 extwwlkfab.c $⊢ C = v ∈ V , n ∈ ℤ ≥ 2 ⟼ w ∈ v ClWWalksNOn ⁡ G n | w ⁡ n − 2 = v$
3 extwwlkfab.f $⊢ F = X ClWWalksNOn ⁡ G N − 2$
4 numclwwlk.t $⊢ T = u ∈ X C N ⟼ u prefix N − 2 u ⁡ N − 1$
5 1 2 3 4 numclwwlk1lem2f1 $⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → T : X C N ⟶ 1-1 F × G NeighbVtx X$
6 1 2 3 4 numclwwlk1lem2fo $⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → T : X C N ⟶ onto F × G NeighbVtx X$
7 df-f1o $⊢ T : X C N ⟶ 1-1 onto F × G NeighbVtx X ↔ T : X C N ⟶ 1-1 F × G NeighbVtx X ∧ T : X C N ⟶ onto F × G NeighbVtx X$
8 5 6 7 sylanbrc $⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → T : X C N ⟶ 1-1 onto F × G NeighbVtx X$