Metamath Proof Explorer

Theorem numclwlk2lem2f1o

Description: R is a 1-1 onto function. (Contributed by Alexander van der Vekens, 6-Oct-2018) (Revised by AV, 21-Jan-2022) (Proof shortened by AV, 17-Mar-2022) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses numclwwlk.v 
|- V = ( Vtx ` G )
numclwwlk.q 
|- Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
numclwwlk.h 
|- H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
numclwwlk.r 
|- R = ( x e. ( X H ( N + 2 ) ) |-> ( x prefix ( N + 1 ) ) )
Assertion numclwlk2lem2f1o 
|- ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> R : ( X H ( N + 2 ) ) -1-1-onto-> ( X Q N ) )

Proof

Step Hyp Ref Expression
1 numclwwlk.v 
 |-  V = ( Vtx ` G )
2 numclwwlk.q 
 |-  Q = ( v e. V , n e. NN |-> { w e. ( n WWalksN G ) | ( ( w ` 0 ) = v /\ ( lastS ` w ) =/= v ) } )
3 numclwwlk.h 
 |-  H = ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
4 numclwwlk.r 
 |-  R = ( x e. ( X H ( N + 2 ) ) |-> ( x prefix ( N + 1 ) ) )
5 eleq1w 
 |-  ( y = x -> ( y e. ( X H ( N + 2 ) ) <-> x e. ( X H ( N + 2 ) ) ) )
6 fveq2 
 |-  ( y = x -> ( R ` y ) = ( R ` x ) )
7 oveq1 
 |-  ( y = x -> ( y prefix ( N + 1 ) ) = ( x prefix ( N + 1 ) ) )
8 6 7 eqeq12d 
 |-  ( y = x -> ( ( R ` y ) = ( y prefix ( N + 1 ) ) <-> ( R ` x ) = ( x prefix ( N + 1 ) ) ) )
9 5 8 imbi12d 
 |-  ( y = x -> ( ( y e. ( X H ( N + 2 ) ) -> ( R ` y ) = ( y prefix ( N + 1 ) ) ) <-> ( x e. ( X H ( N + 2 ) ) -> ( R ` x ) = ( x prefix ( N + 1 ) ) ) ) )
10 9 imbi2d 
 |-  ( y = x -> ( ( ( X e. V /\ N e. NN ) -> ( y e. ( X H ( N + 2 ) ) -> ( R ` y ) = ( y prefix ( N + 1 ) ) ) ) <-> ( ( X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) -> ( R ` x ) = ( x prefix ( N + 1 ) ) ) ) ) )
11 1 2 3 4 numclwlk2lem2fv 
 |-  ( ( X e. V /\ N e. NN ) -> ( y e. ( X H ( N + 2 ) ) -> ( R ` y ) = ( y prefix ( N + 1 ) ) ) )
12 10 11 chvarvv 
 |-  ( ( X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) -> ( R ` x ) = ( x prefix ( N + 1 ) ) ) )
13 12 3adant1 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) -> ( R ` x ) = ( x prefix ( N + 1 ) ) ) )
14 13 imp 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( R ` x ) = ( x prefix ( N + 1 ) ) )
15 1 2 3 4 numclwlk2lem2f 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> R : ( X H ( N + 2 ) ) --> ( X Q N ) )
16 15 ffvelrnda 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( R ` x ) e. ( X Q N ) )
17 14 16 eqeltrrd 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ x e. ( X H ( N + 2 ) ) ) -> ( x prefix ( N + 1 ) ) e. ( X Q N ) )
18 17 ralrimiva 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> A. x e. ( X H ( N + 2 ) ) ( x prefix ( N + 1 ) ) e. ( X Q N ) )
19 1 2 3 numclwwlk2lem1 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( u e. ( X Q N ) -> E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) ) )
20 19 imp 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ u e. ( X Q N ) ) -> E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) )
21 1 2 numclwwlkovq 
 |-  ( ( X e. V /\ N e. NN ) -> ( X Q N ) = { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } )
22 21 eleq2d 
 |-  ( ( X e. V /\ N e. NN ) -> ( u e. ( X Q N ) <-> u e. { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) )
23 22 3adant1 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( u e. ( X Q N ) <-> u e. { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } ) )
24 fveq1 
 |-  ( w = u -> ( w ` 0 ) = ( u ` 0 ) )
25 24 eqeq1d 
 |-  ( w = u -> ( ( w ` 0 ) = X <-> ( u ` 0 ) = X ) )
26 fveq2 
 |-  ( w = u -> ( lastS ` w ) = ( lastS ` u ) )
27 26 neeq1d 
 |-  ( w = u -> ( ( lastS ` w ) =/= X <-> ( lastS ` u ) =/= X ) )
28 25 27 anbi12d 
 |-  ( w = u -> ( ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) <-> ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) )
29 28 elrab 
 |-  ( u e. { w e. ( N WWalksN G ) | ( ( w ` 0 ) = X /\ ( lastS ` w ) =/= X ) } <-> ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) )
30 23 29 bitrdi 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( u e. ( X Q N ) <-> ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) ) )
31 wwlknbp1 
 |-  ( u e. ( N WWalksN G ) -> ( N e. NN0 /\ u e. Word ( Vtx ` G ) /\ ( # ` u ) = ( N + 1 ) ) )
32 3simpc 
 |-  ( ( N e. NN0 /\ u e. Word ( Vtx ` G ) /\ ( # ` u ) = ( N + 1 ) ) -> ( u e. Word ( Vtx ` G ) /\ ( # ` u ) = ( N + 1 ) ) )
33 31 32 syl 
 |-  ( u e. ( N WWalksN G ) -> ( u e. Word ( Vtx ` G ) /\ ( # ` u ) = ( N + 1 ) ) )
34 1 wrdeqi 
 |-  Word V = Word ( Vtx ` G )
35 34 eleq2i 
 |-  ( u e. Word V <-> u e. Word ( Vtx ` G ) )
36 35 anbi1i 
 |-  ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) <-> ( u e. Word ( Vtx ` G ) /\ ( # ` u ) = ( N + 1 ) ) )
37 33 36 sylibr 
 |-  ( u e. ( N WWalksN G ) -> ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) )
38 simpll 
 |-  ( ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> u e. Word V )
39 nnnn0 
 |-  ( N e. NN -> N e. NN0 )
40 2nn 
 |-  2 e. NN
41 40 a1i 
 |-  ( N e. NN -> 2 e. NN )
42 41 nnzd 
 |-  ( N e. NN -> 2 e. ZZ )
43 nn0pzuz 
 |-  ( ( N e. NN0 /\ 2 e. ZZ ) -> ( N + 2 ) e. ( ZZ>= ` 2 ) )
44 39 42 43 syl2anc 
 |-  ( N e. NN -> ( N + 2 ) e. ( ZZ>= ` 2 ) )
45 3 numclwwlkovh 
 |-  ( ( X e. V /\ ( N + 2 ) e. ( ZZ>= ` 2 ) ) -> ( X H ( N + 2 ) ) = { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } )
46 44 45 sylan2 
 |-  ( ( X e. V /\ N e. NN ) -> ( X H ( N + 2 ) ) = { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } )
47 46 eleq2d 
 |-  ( ( X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) <-> x e. { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } ) )
48 fveq1 
 |-  ( w = x -> ( w ` 0 ) = ( x ` 0 ) )
49 48 eqeq1d 
 |-  ( w = x -> ( ( w ` 0 ) = X <-> ( x ` 0 ) = X ) )
50 fveq1 
 |-  ( w = x -> ( w ` ( ( N + 2 ) - 2 ) ) = ( x ` ( ( N + 2 ) - 2 ) ) )
51 50 48 neeq12d 
 |-  ( w = x -> ( ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) <-> ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) )
52 49 51 anbi12d 
 |-  ( w = x -> ( ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) <-> ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) )
53 52 elrab 
 |-  ( x e. { w e. ( ( N + 2 ) ClWWalksN G ) | ( ( w ` 0 ) = X /\ ( w ` ( ( N + 2 ) - 2 ) ) =/= ( w ` 0 ) ) } <-> ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) )
54 47 53 bitrdi 
 |-  ( ( X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) <-> ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) )
55 54 3adant1 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( x e. ( X H ( N + 2 ) ) <-> ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) )
56 55 adantl 
 |-  ( ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> ( x e. ( X H ( N + 2 ) ) <-> ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) ) )
57 1 clwwlknbp 
 |-  ( x e. ( ( N + 2 ) ClWWalksN G ) -> ( x e. Word V /\ ( # ` x ) = ( N + 2 ) ) )
58 lencl 
 |-  ( u e. Word V -> ( # ` u ) e. NN0 )
59 simprr 
 |-  ( ( ( ( ( # ` u ) e. NN0 /\ ( # ` u ) = ( N + 1 ) ) /\ N e. NN ) /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> x e. Word V )
60 df-2 
 |-  2 = ( 1 + 1 )
61 60 a1i 
 |-  ( N e. NN -> 2 = ( 1 + 1 ) )
62 61 oveq2d 
 |-  ( N e. NN -> ( N + 2 ) = ( N + ( 1 + 1 ) ) )
63 nncn 
 |-  ( N e. NN -> N e. CC )
64 1cnd 
 |-  ( N e. NN -> 1 e. CC )
65 63 64 64 addassd 
 |-  ( N e. NN -> ( ( N + 1 ) + 1 ) = ( N + ( 1 + 1 ) ) )
66 62 65 eqtr4d 
 |-  ( N e. NN -> ( N + 2 ) = ( ( N + 1 ) + 1 ) )
67 66 adantl 
 |-  ( ( ( ( # ` u ) e. NN0 /\ ( # ` u ) = ( N + 1 ) ) /\ N e. NN ) -> ( N + 2 ) = ( ( N + 1 ) + 1 ) )
68 67 eqeq2d 
 |-  ( ( ( ( # ` u ) e. NN0 /\ ( # ` u ) = ( N + 1 ) ) /\ N e. NN ) -> ( ( # ` x ) = ( N + 2 ) <-> ( # ` x ) = ( ( N + 1 ) + 1 ) ) )
69 68 biimpcd 
 |-  ( ( # ` x ) = ( N + 2 ) -> ( ( ( ( # ` u ) e. NN0 /\ ( # ` u ) = ( N + 1 ) ) /\ N e. NN ) -> ( # ` x ) = ( ( N + 1 ) + 1 ) ) )
70 69 adantr 
 |-  ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( ( ( # ` u ) e. NN0 /\ ( # ` u ) = ( N + 1 ) ) /\ N e. NN ) -> ( # ` x ) = ( ( N + 1 ) + 1 ) ) )
71 70 impcom 
 |-  ( ( ( ( ( # ` u ) e. NN0 /\ ( # ` u ) = ( N + 1 ) ) /\ N e. NN ) /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( # ` x ) = ( ( N + 1 ) + 1 ) )
72 oveq1 
 |-  ( ( # ` u ) = ( N + 1 ) -> ( ( # ` u ) + 1 ) = ( ( N + 1 ) + 1 ) )
73 72 ad3antlr 
 |-  ( ( ( ( ( # ` u ) e. NN0 /\ ( # ` u ) = ( N + 1 ) ) /\ N e. NN ) /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( ( # ` u ) + 1 ) = ( ( N + 1 ) + 1 ) )
74 71 73 eqtr4d 
 |-  ( ( ( ( ( # ` u ) e. NN0 /\ ( # ` u ) = ( N + 1 ) ) /\ N e. NN ) /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( # ` x ) = ( ( # ` u ) + 1 ) )
75 59 74 jca 
 |-  ( ( ( ( ( # ` u ) e. NN0 /\ ( # ` u ) = ( N + 1 ) ) /\ N e. NN ) /\ ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) )
76 75 exp31 
 |-  ( ( ( # ` u ) e. NN0 /\ ( # ` u ) = ( N + 1 ) ) -> ( N e. NN -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) ) )
77 58 76 sylan 
 |-  ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) -> ( N e. NN -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) ) )
78 77 com12 
 |-  ( N e. NN -> ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) ) )
79 78 3ad2ant3 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) ) )
80 79 impcom 
 |-  ( ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) )
81 80 com12 
 |-  ( ( ( # ` x ) = ( N + 2 ) /\ x e. Word V ) -> ( ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) )
82 81 ancoms 
 |-  ( ( x e. Word V /\ ( # ` x ) = ( N + 2 ) ) -> ( ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) )
83 57 82 syl 
 |-  ( x e. ( ( N + 2 ) ClWWalksN G ) -> ( ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) )
84 83 adantr 
 |-  ( ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) )
85 84 com12 
 |-  ( ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> ( ( x e. ( ( N + 2 ) ClWWalksN G ) /\ ( ( x ` 0 ) = X /\ ( x ` ( ( N + 2 ) - 2 ) ) =/= ( x ` 0 ) ) ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) )
86 56 85 sylbid 
 |-  ( ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> ( x e. ( X H ( N + 2 ) ) -> ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) )
87 86 ralrimiv 
 |-  ( ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> A. x e. ( X H ( N + 2 ) ) ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) )
88 38 87 jca 
 |-  ( ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> ( u e. Word V /\ A. x e. ( X H ( N + 2 ) ) ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) )
89 88 ex 
 |-  ( ( u e. Word V /\ ( # ` u ) = ( N + 1 ) ) -> ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( u e. Word V /\ A. x e. ( X H ( N + 2 ) ) ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) ) )
90 37 89 syl 
 |-  ( u e. ( N WWalksN G ) -> ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( u e. Word V /\ A. x e. ( X H ( N + 2 ) ) ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) ) )
91 90 adantr 
 |-  ( ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) -> ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( u e. Word V /\ A. x e. ( X H ( N + 2 ) ) ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) ) )
92 91 imp 
 |-  ( ( ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> ( u e. Word V /\ A. x e. ( X H ( N + 2 ) ) ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) )
93 nfcv 
 |-  F/_ v X
94 nfmpo1 
 |-  F/_ v ( v e. V , n e. ( ZZ>= ` 2 ) |-> { w e. ( v ( ClWWalksNOn ` G ) n ) | ( w ` ( n - 2 ) ) =/= v } )
95 3 94 nfcxfr 
 |-  F/_ v H
96 nfcv 
 |-  F/_ v ( N + 2 )
97 93 95 96 nfov 
 |-  F/_ v ( X H ( N + 2 ) )
98 97 reuccatpfxs1 
 |-  ( ( u e. Word V /\ A. x e. ( X H ( N + 2 ) ) ( x e. Word V /\ ( # ` x ) = ( ( # ` u ) + 1 ) ) ) -> ( E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) -> E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( # ` u ) ) ) )
99 92 98 syl 
 |-  ( ( ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) -> ( E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) -> E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( # ` u ) ) ) )
100 99 imp 
 |-  ( ( ( ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) /\ E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) ) -> E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( # ` u ) ) )
101 31 simp3d 
 |-  ( u e. ( N WWalksN G ) -> ( # ` u ) = ( N + 1 ) )
102 101 eqcomd 
 |-  ( u e. ( N WWalksN G ) -> ( N + 1 ) = ( # ` u ) )
103 102 ad4antr 
 |-  ( ( ( ( ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) /\ E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) ) /\ x e. ( X H ( N + 2 ) ) ) -> ( N + 1 ) = ( # ` u ) )
104 103 oveq2d 
 |-  ( ( ( ( ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) /\ E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) ) /\ x e. ( X H ( N + 2 ) ) ) -> ( x prefix ( N + 1 ) ) = ( x prefix ( # ` u ) ) )
105 104 eqeq2d 
 |-  ( ( ( ( ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) /\ E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) ) /\ x e. ( X H ( N + 2 ) ) ) -> ( u = ( x prefix ( N + 1 ) ) <-> u = ( x prefix ( # ` u ) ) ) )
106 105 reubidva 
 |-  ( ( ( ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) /\ E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) ) -> ( E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( N + 1 ) ) <-> E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( # ` u ) ) ) )
107 100 106 mpbird 
 |-  ( ( ( ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) /\ ( G e. FriendGraph /\ X e. V /\ N e. NN ) ) /\ E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) ) -> E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( N + 1 ) ) )
108 107 exp31 
 |-  ( ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) -> ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) -> E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( N + 1 ) ) ) ) )
109 108 com12 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( ( u e. ( N WWalksN G ) /\ ( ( u ` 0 ) = X /\ ( lastS ` u ) =/= X ) ) -> ( E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) -> E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( N + 1 ) ) ) ) )
110 30 109 sylbid 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> ( u e. ( X Q N ) -> ( E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) -> E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( N + 1 ) ) ) ) )
111 110 imp 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ u e. ( X Q N ) ) -> ( E! v e. V ( u ++ <" v "> ) e. ( X H ( N + 2 ) ) -> E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( N + 1 ) ) ) )
112 20 111 mpd 
 |-  ( ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) /\ u e. ( X Q N ) ) -> E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( N + 1 ) ) )
113 112 ralrimiva 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> A. u e. ( X Q N ) E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( N + 1 ) ) )
114 4 f1ompt 
 |-  ( R : ( X H ( N + 2 ) ) -1-1-onto-> ( X Q N ) <-> ( A. x e. ( X H ( N + 2 ) ) ( x prefix ( N + 1 ) ) e. ( X Q N ) /\ A. u e. ( X Q N ) E! x e. ( X H ( N + 2 ) ) u = ( x prefix ( N + 1 ) ) ) )
115 18 113 114 sylanbrc 
 |-  ( ( G e. FriendGraph /\ X e. V /\ N e. NN ) -> R : ( X H ( N + 2 ) ) -1-1-onto-> ( X Q N ) )