Metamath Proof Explorer

Theorem clwlkclwwlkf1

Description: F is a one-to-one function from the nonempty closed walks into the closed walks as words in a simple pseudograph. (Contributed by Alexander van der Vekens, 5-Jul-2018) (Revised by AV, 3-May-2021) (Revised by AV, 29-Oct-2022)

Ref Expression
Hypotheses clwlkclwwlkf.c 
|- C = { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) }
clwlkclwwlkf.f 
|- F = ( c e. C |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
Assertion clwlkclwwlkf1 
|- ( G e. USPGraph -> F : C -1-1-> ( ClWWalks ` G ) )

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c 
 |-  C = { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) }
2 clwlkclwwlkf.f 
 |-  F = ( c e. C |-> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) )
3 1 2 clwlkclwwlkf 
 |-  ( G e. USPGraph -> F : C --> ( ClWWalks ` G ) )
4 fveq2 
 |-  ( c = x -> ( 2nd ` c ) = ( 2nd ` x ) )
5 2fveq3 
 |-  ( c = x -> ( # ` ( 2nd ` c ) ) = ( # ` ( 2nd ` x ) ) )
6 5 oveq1d 
 |-  ( c = x -> ( ( # ` ( 2nd ` c ) ) - 1 ) = ( ( # ` ( 2nd ` x ) ) - 1 ) )
7 4 6 oveq12d 
 |-  ( c = x -> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) = ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) )
8 id 
 |-  ( x e. C -> x e. C )
9 ovexd 
 |-  ( x e. C -> ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) e. _V )
10 2 7 8 9 fvmptd3 
 |-  ( x e. C -> ( F ` x ) = ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) )
11 fveq2 
 |-  ( c = y -> ( 2nd ` c ) = ( 2nd ` y ) )
12 2fveq3 
 |-  ( c = y -> ( # ` ( 2nd ` c ) ) = ( # ` ( 2nd ` y ) ) )
13 12 oveq1d 
 |-  ( c = y -> ( ( # ` ( 2nd ` c ) ) - 1 ) = ( ( # ` ( 2nd ` y ) ) - 1 ) )
14 11 13 oveq12d 
 |-  ( c = y -> ( ( 2nd ` c ) prefix ( ( # ` ( 2nd ` c ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) )
15 id 
 |-  ( y e. C -> y e. C )
16 ovexd 
 |-  ( y e. C -> ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) e. _V )
17 2 14 15 16 fvmptd3 
 |-  ( y e. C -> ( F ` y ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) )
18 10 17 eqeqan12d 
 |-  ( ( x e. C /\ y e. C ) -> ( ( F ` x ) = ( F ` y ) <-> ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) ) )
19 18 adantl 
 |-  ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) -> ( ( F ` x ) = ( F ` y ) <-> ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) ) )
20 simplrl 
 |-  ( ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) /\ ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) ) -> x e. C )
21 simplrr 
 |-  ( ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) /\ ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) ) -> y e. C )
22 eqid 
 |-  ( 1st ` x ) = ( 1st ` x )
23 eqid 
 |-  ( 2nd ` x ) = ( 2nd ` x )
24 1 22 23 clwlkclwwlkflem 
 |-  ( x e. C -> ( ( 1st ` x ) ( Walks ` G ) ( 2nd ` x ) /\ ( ( 2nd ` x ) ` 0 ) = ( ( 2nd ` x ) ` ( # ` ( 1st ` x ) ) ) /\ ( # ` ( 1st ` x ) ) e. NN ) )
25 wlklenvm1 
 |-  ( ( 1st ` x ) ( Walks ` G ) ( 2nd ` x ) -> ( # ` ( 1st ` x ) ) = ( ( # ` ( 2nd ` x ) ) - 1 ) )
26 25 eqcomd 
 |-  ( ( 1st ` x ) ( Walks ` G ) ( 2nd ` x ) -> ( ( # ` ( 2nd ` x ) ) - 1 ) = ( # ` ( 1st ` x ) ) )
27 26 3ad2ant1 
 |-  ( ( ( 1st ` x ) ( Walks ` G ) ( 2nd ` x ) /\ ( ( 2nd ` x ) ` 0 ) = ( ( 2nd ` x ) ` ( # ` ( 1st ` x ) ) ) /\ ( # ` ( 1st ` x ) ) e. NN ) -> ( ( # ` ( 2nd ` x ) ) - 1 ) = ( # ` ( 1st ` x ) ) )
28 24 27 syl 
 |-  ( x e. C -> ( ( # ` ( 2nd ` x ) ) - 1 ) = ( # ` ( 1st ` x ) ) )
29 28 adantr 
 |-  ( ( x e. C /\ y e. C ) -> ( ( # ` ( 2nd ` x ) ) - 1 ) = ( # ` ( 1st ` x ) ) )
30 29 oveq2d 
 |-  ( ( x e. C /\ y e. C ) -> ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` x ) prefix ( # ` ( 1st ` x ) ) ) )
31 eqid 
 |-  ( 1st ` y ) = ( 1st ` y )
32 eqid 
 |-  ( 2nd ` y ) = ( 2nd ` y )
33 1 31 32 clwlkclwwlkflem 
 |-  ( y e. C -> ( ( 1st ` y ) ( Walks ` G ) ( 2nd ` y ) /\ ( ( 2nd ` y ) ` 0 ) = ( ( 2nd ` y ) ` ( # ` ( 1st ` y ) ) ) /\ ( # ` ( 1st ` y ) ) e. NN ) )
34 wlklenvm1 
 |-  ( ( 1st ` y ) ( Walks ` G ) ( 2nd ` y ) -> ( # ` ( 1st ` y ) ) = ( ( # ` ( 2nd ` y ) ) - 1 ) )
35 34 eqcomd 
 |-  ( ( 1st ` y ) ( Walks ` G ) ( 2nd ` y ) -> ( ( # ` ( 2nd ` y ) ) - 1 ) = ( # ` ( 1st ` y ) ) )
36 35 3ad2ant1 
 |-  ( ( ( 1st ` y ) ( Walks ` G ) ( 2nd ` y ) /\ ( ( 2nd ` y ) ` 0 ) = ( ( 2nd ` y ) ` ( # ` ( 1st ` y ) ) ) /\ ( # ` ( 1st ` y ) ) e. NN ) -> ( ( # ` ( 2nd ` y ) ) - 1 ) = ( # ` ( 1st ` y ) ) )
37 33 36 syl 
 |-  ( y e. C -> ( ( # ` ( 2nd ` y ) ) - 1 ) = ( # ` ( 1st ` y ) ) )
38 37 adantl 
 |-  ( ( x e. C /\ y e. C ) -> ( ( # ` ( 2nd ` y ) ) - 1 ) = ( # ` ( 1st ` y ) ) )
39 38 oveq2d 
 |-  ( ( x e. C /\ y e. C ) -> ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( # ` ( 1st ` y ) ) ) )
40 30 39 eqeq12d 
 |-  ( ( x e. C /\ y e. C ) -> ( ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) <-> ( ( 2nd ` x ) prefix ( # ` ( 1st ` x ) ) ) = ( ( 2nd ` y ) prefix ( # ` ( 1st ` y ) ) ) ) )
41 40 adantl 
 |-  ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) -> ( ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) <-> ( ( 2nd ` x ) prefix ( # ` ( 1st ` x ) ) ) = ( ( 2nd ` y ) prefix ( # ` ( 1st ` y ) ) ) ) )
42 41 biimpa 
 |-  ( ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) /\ ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) ) -> ( ( 2nd ` x ) prefix ( # ` ( 1st ` x ) ) ) = ( ( 2nd ` y ) prefix ( # ` ( 1st ` y ) ) ) )
43 20 21 42 3jca 
 |-  ( ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) /\ ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) ) -> ( x e. C /\ y e. C /\ ( ( 2nd ` x ) prefix ( # ` ( 1st ` x ) ) ) = ( ( 2nd ` y ) prefix ( # ` ( 1st ` y ) ) ) ) )
44 1 22 23 31 32 clwlkclwwlkf1lem2 
 |-  ( ( x e. C /\ y e. C /\ ( ( 2nd ` x ) prefix ( # ` ( 1st ` x ) ) ) = ( ( 2nd ` y ) prefix ( # ` ( 1st ` y ) ) ) ) -> ( ( # ` ( 1st ` x ) ) = ( # ` ( 1st ` y ) ) /\ A. i e. ( 0 ..^ ( # ` ( 1st ` x ) ) ) ( ( 2nd ` x ) ` i ) = ( ( 2nd ` y ) ` i ) ) )
45 simpl 
 |-  ( ( ( # ` ( 1st ` x ) ) = ( # ` ( 1st ` y ) ) /\ A. i e. ( 0 ..^ ( # ` ( 1st ` x ) ) ) ( ( 2nd ` x ) ` i ) = ( ( 2nd ` y ) ` i ) ) -> ( # ` ( 1st ` x ) ) = ( # ` ( 1st ` y ) ) )
46 43 44 45 3syl 
 |-  ( ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) /\ ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) ) -> ( # ` ( 1st ` x ) ) = ( # ` ( 1st ` y ) ) )
47 1 22 23 31 32 clwlkclwwlkf1lem3 
 |-  ( ( x e. C /\ y e. C /\ ( ( 2nd ` x ) prefix ( # ` ( 1st ` x ) ) ) = ( ( 2nd ` y ) prefix ( # ` ( 1st ` y ) ) ) ) -> A. i e. ( 0 ... ( # ` ( 1st ` x ) ) ) ( ( 2nd ` x ) ` i ) = ( ( 2nd ` y ) ` i ) )
48 43 47 syl 
 |-  ( ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) /\ ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) ) -> A. i e. ( 0 ... ( # ` ( 1st ` x ) ) ) ( ( 2nd ` x ) ` i ) = ( ( 2nd ` y ) ` i ) )
49 simpl 
 |-  ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) -> G e. USPGraph )
50 wlkcpr 
 |-  ( x e. ( Walks ` G ) <-> ( 1st ` x ) ( Walks ` G ) ( 2nd ` x ) )
51 50 biimpri 
 |-  ( ( 1st ` x ) ( Walks ` G ) ( 2nd ` x ) -> x e. ( Walks ` G ) )
52 51 3ad2ant1 
 |-  ( ( ( 1st ` x ) ( Walks ` G ) ( 2nd ` x ) /\ ( ( 2nd ` x ) ` 0 ) = ( ( 2nd ` x ) ` ( # ` ( 1st ` x ) ) ) /\ ( # ` ( 1st ` x ) ) e. NN ) -> x e. ( Walks ` G ) )
53 24 52 syl 
 |-  ( x e. C -> x e. ( Walks ` G ) )
54 wlkcpr 
 |-  ( y e. ( Walks ` G ) <-> ( 1st ` y ) ( Walks ` G ) ( 2nd ` y ) )
55 54 biimpri 
 |-  ( ( 1st ` y ) ( Walks ` G ) ( 2nd ` y ) -> y e. ( Walks ` G ) )
56 55 3ad2ant1 
 |-  ( ( ( 1st ` y ) ( Walks ` G ) ( 2nd ` y ) /\ ( ( 2nd ` y ) ` 0 ) = ( ( 2nd ` y ) ` ( # ` ( 1st ` y ) ) ) /\ ( # ` ( 1st ` y ) ) e. NN ) -> y e. ( Walks ` G ) )
57 33 56 syl 
 |-  ( y e. C -> y e. ( Walks ` G ) )
58 53 57 anim12i 
 |-  ( ( x e. C /\ y e. C ) -> ( x e. ( Walks ` G ) /\ y e. ( Walks ` G ) ) )
59 58 adantl 
 |-  ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) -> ( x e. ( Walks ` G ) /\ y e. ( Walks ` G ) ) )
60 eqidd 
 |-  ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) -> ( # ` ( 1st ` x ) ) = ( # ` ( 1st ` x ) ) )
61 49 59 60 3jca 
 |-  ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) -> ( G e. USPGraph /\ ( x e. ( Walks ` G ) /\ y e. ( Walks ` G ) ) /\ ( # ` ( 1st ` x ) ) = ( # ` ( 1st ` x ) ) ) )
62 61 adantr 
 |-  ( ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) /\ ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) ) -> ( G e. USPGraph /\ ( x e. ( Walks ` G ) /\ y e. ( Walks ` G ) ) /\ ( # ` ( 1st ` x ) ) = ( # ` ( 1st ` x ) ) ) )
63 uspgr2wlkeq 
 |-  ( ( G e. USPGraph /\ ( x e. ( Walks ` G ) /\ y e. ( Walks ` G ) ) /\ ( # ` ( 1st ` x ) ) = ( # ` ( 1st ` x ) ) ) -> ( x = y <-> ( ( # ` ( 1st ` x ) ) = ( # ` ( 1st ` y ) ) /\ A. i e. ( 0 ... ( # ` ( 1st ` x ) ) ) ( ( 2nd ` x ) ` i ) = ( ( 2nd ` y ) ` i ) ) ) )
64 62 63 syl 
 |-  ( ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) /\ ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) ) -> ( x = y <-> ( ( # ` ( 1st ` x ) ) = ( # ` ( 1st ` y ) ) /\ A. i e. ( 0 ... ( # ` ( 1st ` x ) ) ) ( ( 2nd ` x ) ` i ) = ( ( 2nd ` y ) ` i ) ) ) )
65 46 48 64 mpbir2and 
 |-  ( ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) /\ ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) ) -> x = y )
66 65 ex 
 |-  ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) -> ( ( ( 2nd ` x ) prefix ( ( # ` ( 2nd ` x ) ) - 1 ) ) = ( ( 2nd ` y ) prefix ( ( # ` ( 2nd ` y ) ) - 1 ) ) -> x = y ) )
67 19 66 sylbid 
 |-  ( ( G e. USPGraph /\ ( x e. C /\ y e. C ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
68 67 ralrimivva 
 |-  ( G e. USPGraph -> A. x e. C A. y e. C ( ( F ` x ) = ( F ` y ) -> x = y ) )
69 dff13 
 |-  ( F : C -1-1-> ( ClWWalks ` G ) <-> ( F : C --> ( ClWWalks ` G ) /\ A. x e. C A. y e. C ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
70 3 68 69 sylanbrc 
 |-  ( G e. USPGraph -> F : C -1-1-> ( ClWWalks ` G ) )