Metamath Proof Explorer

Theorem numclwwlk1lem2fo

Description: T is an onto function. (Contributed by Alexander van der Vekens, 20-Sep-2018) (Revised by AV, 29-May-2021) (Proof shortened by AV, 13-Feb-2022) (Revised by AV, 31-Oct-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 numclwwlk1lem2fo 
|- ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> T : ( X C N ) -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 numclwwlk1lem2f 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> T : ( X C N ) --> ( F X. ( G NeighbVtx X ) ) )
6 elxp 
 |-  ( p e. ( F X. ( G NeighbVtx X ) ) <-> E. a E. b ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) )
7 1 2 3 numclwwlk1lem2foa 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a e. F /\ b e. ( G NeighbVtx X ) ) -> ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) ) )
8 7 com12 
 |-  ( ( a e. F /\ b e. ( G NeighbVtx X ) ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) ) )
9 8 adantl 
 |-  ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) ) )
10 9 imp 
 |-  ( ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) )
11 simpl 
 |-  ( ( ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) /\ ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) ) -> ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) )
12 fveq2 
 |-  ( x = ( ( a ++ <" X "> ) ++ <" b "> ) -> ( T ` x ) = ( T ` ( ( a ++ <" X "> ) ++ <" b "> ) ) )
13 12 eqeq2d 
 |-  ( x = ( ( a ++ <" X "> ) ++ <" b "> ) -> ( p = ( T ` x ) <-> p = ( T ` ( ( a ++ <" X "> ) ++ <" b "> ) ) ) )
14 1 2 3 4 numclwwlk1lem2fv 
 |-  ( ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) -> ( T ` ( ( a ++ <" X "> ) ++ <" b "> ) ) = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. )
15 14 adantr 
 |-  ( ( ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) /\ ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) ) -> ( T ` ( ( a ++ <" X "> ) ++ <" b "> ) ) = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. )
16 15 eqeq2d 
 |-  ( ( ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) /\ ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) ) -> ( p = ( T ` ( ( a ++ <" X "> ) ++ <" b "> ) ) <-> p = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) )
17 13 16 sylan9bbr 
 |-  ( ( ( ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) /\ ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) ) /\ x = ( ( a ++ <" X "> ) ++ <" b "> ) ) -> ( p = ( T ` x ) <-> p = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) )
18 simprll 
 |-  ( ( ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) /\ ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) ) -> p = <. a , b >. )
19 1 nbgrisvtx 
 |-  ( b e. ( G NeighbVtx X ) -> b e. V )
20 3 eleq2i 
 |-  ( a e. F <-> a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) )
21 uz3m2nn 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) e. NN )
22 21 nnne0d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 2 ) =/= 0 )
23 22 3ad2ant3 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 2 ) =/= 0 )
24 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
25 1 24 clwwlknonel 
 |-  ( ( N - 2 ) =/= 0 -> ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) <-> ( ( a e. Word V /\ A. i e. ( 0 ..^ ( ( # ` a ) - 1 ) ) { ( a ` i ) , ( a ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` a ) , ( a ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` a ) = ( N - 2 ) /\ ( a ` 0 ) = X ) ) )
26 23 25 syl 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( a e. ( X ( ClWWalksNOn ` G ) ( N - 2 ) ) <-> ( ( a e. Word V /\ A. i e. ( 0 ..^ ( ( # ` a ) - 1 ) ) { ( a ` i ) , ( a ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` a ) , ( a ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` a ) = ( N - 2 ) /\ ( a ` 0 ) = X ) ) )
27 20 26 syl5bb 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( a e. F <-> ( ( a e. Word V /\ A. i e. ( 0 ..^ ( ( # ` a ) - 1 ) ) { ( a ` i ) , ( a ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` a ) , ( a ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` a ) = ( N - 2 ) /\ ( a ` 0 ) = X ) ) )
28 df-3an 
 |-  ( ( ( a e. Word V /\ A. i e. ( 0 ..^ ( ( # ` a ) - 1 ) ) { ( a ` i ) , ( a ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` a ) , ( a ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` a ) = ( N - 2 ) /\ ( a ` 0 ) = X ) <-> ( ( ( a e. Word V /\ A. i e. ( 0 ..^ ( ( # ` a ) - 1 ) ) { ( a ` i ) , ( a ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` a ) , ( a ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` a ) = ( N - 2 ) ) /\ ( a ` 0 ) = X ) )
29 27 28 syl6bb 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( a e. F <-> ( ( ( a e. Word V /\ A. i e. ( 0 ..^ ( ( # ` a ) - 1 ) ) { ( a ` i ) , ( a ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` a ) , ( a ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` a ) = ( N - 2 ) ) /\ ( a ` 0 ) = X ) ) )
30 simplll 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> a e. Word V )
31 s1cl 
 |-  ( X e. V -> <" X "> e. Word V )
32 31 adantr 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> <" X "> e. Word V )
33 32 adantl 
 |-  ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> <" X "> e. Word V )
34 33 adantr 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> <" X "> e. Word V )
35 s1cl 
 |-  ( b e. V -> <" b "> e. Word V )
36 35 adantl 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> <" b "> e. Word V )
37 ccatass 
 |-  ( ( a e. Word V /\ <" X "> e. Word V /\ <" b "> e. Word V ) -> ( ( a ++ <" X "> ) ++ <" b "> ) = ( a ++ ( <" X "> ++ <" b "> ) ) )
38 37 oveq1d 
 |-  ( ( a e. Word V /\ <" X "> e. Word V /\ <" b "> e. Word V ) -> ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) = ( ( a ++ ( <" X "> ++ <" b "> ) ) prefix ( N - 2 ) ) )
39 30 34 36 38 syl3anc 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) = ( ( a ++ ( <" X "> ++ <" b "> ) ) prefix ( N - 2 ) ) )
40 ccatcl 
 |-  ( ( <" X "> e. Word V /\ <" b "> e. Word V ) -> ( <" X "> ++ <" b "> ) e. Word V )
41 33 35 40 syl2an 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> ( <" X "> ++ <" b "> ) e. Word V )
42 simpr 
 |-  ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) -> ( # ` a ) = ( N - 2 ) )
43 42 eqcomd 
 |-  ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) -> ( N - 2 ) = ( # ` a ) )
44 43 adantr 
 |-  ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( N - 2 ) = ( # ` a ) )
45 44 adantr 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> ( N - 2 ) = ( # ` a ) )
46 pfxccatid 
 |-  ( ( a e. Word V /\ ( <" X "> ++ <" b "> ) e. Word V /\ ( N - 2 ) = ( # ` a ) ) -> ( ( a ++ ( <" X "> ++ <" b "> ) ) prefix ( N - 2 ) ) = a )
47 30 41 45 46 syl3anc 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> ( ( a ++ ( <" X "> ++ <" b "> ) ) prefix ( N - 2 ) ) = a )
48 39 47 eqtr2d 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> a = ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) )
49 1e2m1 
 |-  1 = ( 2 - 1 )
50 49 a1i 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 = ( 2 - 1 ) )
51 50 oveq2d 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) = ( N - ( 2 - 1 ) ) )
52 eluzelcn 
 |-  ( N e. ( ZZ>= ` 3 ) -> N e. CC )
53 2cnd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 2 e. CC )
54 1cnd 
 |-  ( N e. ( ZZ>= ` 3 ) -> 1 e. CC )
55 52 53 54 subsubd 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - ( 2 - 1 ) ) = ( ( N - 2 ) + 1 ) )
56 51 55 eqtrd 
 |-  ( N e. ( ZZ>= ` 3 ) -> ( N - 1 ) = ( ( N - 2 ) + 1 ) )
57 56 adantl 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( N - 1 ) = ( ( N - 2 ) + 1 ) )
58 57 adantl 
 |-  ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> ( N - 1 ) = ( ( N - 2 ) + 1 ) )
59 58 adantr 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> ( N - 1 ) = ( ( N - 2 ) + 1 ) )
60 59 fveq2d 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) = ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( ( N - 2 ) + 1 ) ) )
61 simpll 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) )
62 simprl 
 |-  ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> X e. V )
63 62 anim1i 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> ( X e. V /\ b e. V ) )
64 ccatw2s1p2 
 |-  ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ b e. V ) ) -> ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( ( N - 2 ) + 1 ) ) = b )
65 61 63 64 syl2anc 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( ( N - 2 ) + 1 ) ) = b )
66 60 65 eqtr2d 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> b = ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) )
67 48 66 opeq12d 
 |-  ( ( ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) /\ ( X e. V /\ N e. ( ZZ>= ` 3 ) ) ) /\ b e. V ) -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. )
68 67 exp31 
 |-  ( ( a e. Word V /\ ( # ` a ) = ( N - 2 ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( b e. V -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) ) )
69 68 3ad2antl1 
 |-  ( ( ( a e. Word V /\ A. i e. ( 0 ..^ ( ( # ` a ) - 1 ) ) { ( a ` i ) , ( a ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` a ) , ( a ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` a ) = ( N - 2 ) ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( b e. V -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) ) )
70 69 adantr 
 |-  ( ( ( ( a e. Word V /\ A. i e. ( 0 ..^ ( ( # ` a ) - 1 ) ) { ( a ` i ) , ( a ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` a ) , ( a ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` a ) = ( N - 2 ) ) /\ ( a ` 0 ) = X ) -> ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( b e. V -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) ) )
71 70 com12 
 |-  ( ( X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( ( a e. Word V /\ A. i e. ( 0 ..^ ( ( # ` a ) - 1 ) ) { ( a ` i ) , ( a ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` a ) , ( a ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` a ) = ( N - 2 ) ) /\ ( a ` 0 ) = X ) -> ( b e. V -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) ) )
72 71 3adant1 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( ( ( ( a e. Word V /\ A. i e. ( 0 ..^ ( ( # ` a ) - 1 ) ) { ( a ` i ) , ( a ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` a ) , ( a ` 0 ) } e. ( Edg ` G ) ) /\ ( # ` a ) = ( N - 2 ) ) /\ ( a ` 0 ) = X ) -> ( b e. V -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) ) )
73 29 72 sylbid 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( a e. F -> ( b e. V -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) ) )
74 73 com23 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( b e. V -> ( a e. F -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) ) )
75 19 74 syl5 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> ( b e. ( G NeighbVtx X ) -> ( a e. F -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) ) )
76 75 com13 
 |-  ( a e. F -> ( b e. ( G NeighbVtx X ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) ) )
77 76 imp 
 |-  ( ( a e. F /\ b e. ( G NeighbVtx X ) ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) )
78 77 adantl 
 |-  ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. ) )
79 78 imp 
 |-  ( ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. )
80 79 adantl 
 |-  ( ( ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) /\ ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) ) -> <. a , b >. = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. )
81 18 80 eqtrd 
 |-  ( ( ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) /\ ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) ) -> p = <. ( ( ( a ++ <" X "> ) ++ <" b "> ) prefix ( N - 2 ) ) , ( ( ( a ++ <" X "> ) ++ <" b "> ) ` ( N - 1 ) ) >. )
82 11 17 81 rspcedvd 
 |-  ( ( ( ( a ++ <" X "> ) ++ <" b "> ) e. ( X C N ) /\ ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) ) -> E. x e. ( X C N ) p = ( T ` x ) )
83 10 82 mpancom 
 |-  ( ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) /\ ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) ) -> E. x e. ( X C N ) p = ( T ` x ) )
84 83 ex 
 |-  ( ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> E. x e. ( X C N ) p = ( T ` x ) ) )
85 84 exlimivv 
 |-  ( E. a E. b ( p = <. a , b >. /\ ( a e. F /\ b e. ( G NeighbVtx X ) ) ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> E. x e. ( X C N ) p = ( T ` x ) ) )
86 6 85 sylbi 
 |-  ( p e. ( F X. ( G NeighbVtx X ) ) -> ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> E. x e. ( X C N ) p = ( T ` x ) ) )
87 86 impcom 
 |-  ( ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) /\ p e. ( F X. ( G NeighbVtx X ) ) ) -> E. x e. ( X C N ) p = ( T ` x ) )
88 87 ralrimiva 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> A. p e. ( F X. ( G NeighbVtx X ) ) E. x e. ( X C N ) p = ( T ` x ) )
89 dffo3 
 |-  ( T : ( X C N ) -onto-> ( F X. ( G NeighbVtx X ) ) <-> ( T : ( X C N ) --> ( F X. ( G NeighbVtx X ) ) /\ A. p e. ( F X. ( G NeighbVtx X ) ) E. x e. ( X C N ) p = ( T ` x ) ) )
90 5 88 89 sylanbrc 
 |-  ( ( G e. USGraph /\ X e. V /\ N e. ( ZZ>= ` 3 ) ) -> T : ( X C N ) -onto-> ( F X. ( G NeighbVtx X ) ) )