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 ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
extwwlkfab.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
extwwlkfab.f ⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
numclwwlk.t ⊢ 𝑇 = ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ )
Assertion numclwwlk1lem2f ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) ⟶ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 extwwlkfab.v ⊢ 𝑉 = ( Vtx ‘ 𝐺 )
2 extwwlkfab.c ⊢ 𝐶 = ( 𝑣 ∈ 𝑉 , 𝑛 ∈ ( ℤ≥ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
3 extwwlkfab.f ⊢ 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
4 numclwwlk.t ⊢ 𝑇 = ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ )
5 1 2 3 extwwlkfabel ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ↔ ( 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑢 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑢 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑢 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) ) )
6 simpr1 ⊢ ( ( 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑢 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑢 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑢 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑢 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 )
7 simpr2 ⊢ ( ( 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑢 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑢 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑢 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ( 𝑢 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) )
8 6 7 opelxpd ⊢ ( ( 𝑢 ∈ ( 𝑁 ClWWalksN 𝐺 ) ∧ ( ( 𝑢 prefix ( 𝑁 − 2 ) ) ∈ 𝐹 ∧ ( 𝑢 ‘ ( 𝑁 − 1 ) ) ∈ ( 𝐺 NeighbVtx 𝑋 ) ∧ ( 𝑢 ‘ ( 𝑁 − 2 ) ) = 𝑋 ) ) → ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ ∈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )
9 5 8 biimtrdi ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) → ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ ∈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ) )
10 9 imp ⊢ ( ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) ∧ 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ) → ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ ∈ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )
11 10 4 fmptd ⊢ ( ( 𝐺 ∈ USGraph ∧ 𝑋 ∈ 𝑉 ∧ 𝑁 ∈ ( ℤ≥ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) ⟶ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )