# 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 𝑉 = ( Vtx ‘ 𝐺 )
extwwlkfab.c 𝐶 = ( 𝑣𝑉 , 𝑛 ∈ ( ℤ ‘ 2 ) ↦ { 𝑤 ∈ ( 𝑣 ( ClWWalksNOn ‘ 𝐺 ) 𝑛 ) ∣ ( 𝑤 ‘ ( 𝑛 − 2 ) ) = 𝑣 } )
extwwlkfab.f 𝐹 = ( 𝑋 ( ClWWalksNOn ‘ 𝐺 ) ( 𝑁 − 2 ) )
numclwwlk.t 𝑇 = ( 𝑢 ∈ ( 𝑋 𝐶 𝑁 ) ↦ ⟨ ( 𝑢 prefix ( 𝑁 − 2 ) ) , ( 𝑢 ‘ ( 𝑁 − 1 ) ) ⟩ )
Assertion numclwwlk1lem2f1o ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) –1-1-onto→ ( 𝐹 × ( 𝐺 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 4 numclwwlk1lem2f1 ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) –1-1→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )
6 1 2 3 4 numclwwlk1lem2fo ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) –onto→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )
7 df-f1o ( 𝑇 : ( 𝑋 𝐶 𝑁 ) –1-1-onto→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ↔ ( 𝑇 : ( 𝑋 𝐶 𝑁 ) –1-1→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ∧ 𝑇 : ( 𝑋 𝐶 𝑁 ) –onto→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) ) )
8 5 6 7 sylanbrc ( ( 𝐺 ∈ USGraph ∧ 𝑋𝑉𝑁 ∈ ( ℤ ‘ 3 ) ) → 𝑇 : ( 𝑋 𝐶 𝑁 ) –1-1-onto→ ( 𝐹 × ( 𝐺 NeighbVtx 𝑋 ) ) )