Metamath Proof Explorer

Theorem numclwwlk1lem2f

Description: T is a function, mapping a double loop of length N on vertex X to the ordered pair of the first loop and the successor of X in the second loop, which must be a neighbor of X . (Contributed by Alexander van der Vekens, 19-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 23-Feb-2022) (Revised by AV, 31-Oct-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 numclwwlk1lem2f ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → T : X C N ⟶ 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 extwwlkfabel ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → u ∈ X C N ↔ u ∈ N ClWWalksN G ∧ u prefix N − 2 ∈ F ∧ u ⁡ N − 1 ∈ G NeighbVtx X ∧ u ⁡ N − 2 = X
6 simpr1 ⊢ u ∈ N ClWWalksN G ∧ u prefix N − 2 ∈ F ∧ u ⁡ N − 1 ∈ G NeighbVtx X ∧ u ⁡ N − 2 = X → u prefix N − 2 ∈ F
7 simpr2 ⊢ u ∈ N ClWWalksN G ∧ u prefix N − 2 ∈ F ∧ u ⁡ N − 1 ∈ G NeighbVtx X ∧ u ⁡ N − 2 = X → u ⁡ N − 1 ∈ G NeighbVtx X
8 6 7 opelxpd ⊢ u ∈ N ClWWalksN G ∧ u prefix N − 2 ∈ F ∧ u ⁡ N − 1 ∈ G NeighbVtx X ∧ u ⁡ N − 2 = X → u prefix N − 2 u ⁡ N − 1 ∈ F × G NeighbVtx X
9 5 8 biimtrdi ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → u ∈ X C N → u prefix N − 2 u ⁡ N − 1 ∈ F × G NeighbVtx X
10 9 imp ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 ∧ u ∈ X C N → u prefix N − 2 u ⁡ N − 1 ∈ F × G NeighbVtx X
11 10 4 fmptd ⊢ G ∈ USGraph ∧ X ∈ V ∧ N ∈ ℤ ≥ 3 → T : X C N ⟶ F × G NeighbVtx X