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