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 e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
extwwlkfab.f 
|- F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
numclwwlk.t 
|- T = ( u e. ( X C N ) |-> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. )
Assertion numclwwlk1lem2f1o 
|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> T : ( X C N ) -1-1-onto-> ( F X. ( G NeighbVtx X ) ) )

Proof

Step Hyp Ref Expression
1 extwwlkfab.v 
 |-  V = ( Vtx ` G )
2 extwwlkfab.c 
 |-  C = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) = v } )
3 extwwlkfab.f 
 |-  F = ( X ( ClWWalksNOn ` G ) ( N - 2 ) )
4 numclwwlk.t 
 |-  T = ( u e. ( X C N ) |-> <. ( u prefix ( N - 2 ) ) , ( u ` ( N - 1 ) ) >. )
5 1 2 3 4 numclwwlk1lem2f1 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> T : ( X C N ) -1-1-> ( F X. ( G NeighbVtx X ) ) )
6 1 2 3 4 numclwwlk1lem2fo 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> T : ( X C N ) -onto-> ( F X. ( G NeighbVtx X ) ) )
7 df-f1o 
 |-  ( T : ( X C N ) -1-1-onto-> ( F X. ( G NeighbVtx X ) ) <-> ( T : ( X C N ) -1-1-> ( F X. ( G NeighbVtx X ) ) /\ T : ( X C N ) -onto-> ( F X. ( G NeighbVtx X ) ) ) )
8 5 6 7 sylanbrc 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> T : ( X C N ) -1-1-onto-> ( F X. ( G NeighbVtx X ) ) )