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∈vClWWalksNOn⁡Gn|w⁡n−2=v
extwwlkfab.f ⊢F=XClWWalksNOn⁡GN−2
numclwwlk.t ⊢T=u∈XCN⟼uprefixN−2u⁡N−1
Assertion numclwwlk1lem2f ⊢G∈USGraph∧X∈V∧N∈ℤ≥3→T:XCN⟶F×GNeighbVtxX

Proof

Step Hyp Ref Expression
1 extwwlkfab.v ⊢V=Vtx⁡G
2 extwwlkfab.c ⊢C=v∈V,n∈ℤ≥2⟼w∈vClWWalksNOn⁡Gn|w⁡n−2=v
3 extwwlkfab.f ⊢F=XClWWalksNOn⁡GN−2
4 numclwwlk.t ⊢T=u∈XCN⟼uprefixN−2u⁡N−1
5 1 2 3 extwwlkfabel ⊢G∈USGraph∧X∈V∧N∈ℤ≥3→u∈XCN↔u∈NClWWalksNG∧uprefixN−2∈F∧u⁡N−1∈GNeighbVtxX∧u⁡N−2=X
6 simpr1 ⊢u∈NClWWalksNG∧uprefixN−2∈F∧u⁡N−1∈GNeighbVtxX∧u⁡N−2=X→uprefixN−2∈F
7 simpr2 ⊢u∈NClWWalksNG∧uprefixN−2∈F∧u⁡N−1∈GNeighbVtxX∧u⁡N−2=X→u⁡N−1∈GNeighbVtxX
8 6 7 opelxpd ⊢u∈NClWWalksNG∧uprefixN−2∈F∧u⁡N−1∈GNeighbVtxX∧u⁡N−2=X→uprefixN−2u⁡N−1∈F×GNeighbVtxX
9 5 8 syl6bi ⊢G∈USGraph∧X∈V∧N∈ℤ≥3→u∈XCN→uprefixN−2u⁡N−1∈F×GNeighbVtxX
10 9 imp ⊢G∈USGraph∧X∈V∧N∈ℤ≥3∧u∈XCN→uprefixN−2u⁡N−1∈F×GNeighbVtxX
11 10 4 fmptd ⊢G∈USGraph∧X∈V∧N∈ℤ≥3→T:XCN⟶F×GNeighbVtxX