Metamath Proof Explorer

Theorem wlkswwlksf1o

Description: The mapping of (ordinary) walks to their sequences of vertices is a bijection in a simple pseudograph. (Contributed by AV, 6-May-2021)

Ref Expression
Hypothesis wlkswwlksf1o.f 
|- F = ( w e. ( Walks ` G ) |-> ( 2nd ` w ) )
Assertion wlkswwlksf1o 
|- ( G e. USPGraph -> F : ( Walks ` G ) -1-1-onto-> ( WWalks ` G ) )

Proof

Step Hyp Ref Expression
1 wlkswwlksf1o.f 
 |-  F = ( w e. ( Walks ` G ) |-> ( 2nd ` w ) )
2 fvex 
 |-  ( 1st ` w ) e. _V
3 breq1 
 |-  ( f = ( 1st ` w ) -> ( f ( Walks ` G ) ( 2nd ` w ) <-> ( 1st ` w ) ( Walks ` G ) ( 2nd ` w ) ) )
4 2 3 spcev 
 |-  ( ( 1st ` w ) ( Walks ` G ) ( 2nd ` w ) -> E. f f ( Walks ` G ) ( 2nd ` w ) )
5 wlkiswwlks 
 |-  ( G e. USPGraph -> ( E. f f ( Walks ` G ) ( 2nd ` w ) <-> ( 2nd ` w ) e. ( WWalks ` G ) ) )
6 4 5 imbitrid 
 |-  ( G e. USPGraph -> ( ( 1st ` w ) ( Walks ` G ) ( 2nd ` w ) -> ( 2nd ` w ) e. ( WWalks ` G ) ) )
7 wlkcpr 
 |-  ( w e. ( Walks ` G ) <-> ( 1st ` w ) ( Walks ` G ) ( 2nd ` w ) )
8 7 biimpi 
 |-  ( w e. ( Walks ` G ) -> ( 1st ` w ) ( Walks ` G ) ( 2nd ` w ) )
9 6 8 impel 
 |-  ( ( G e. USPGraph /\ w e. ( Walks ` G ) ) -> ( 2nd ` w ) e. ( WWalks ` G ) )
10 9 1 fmptd 
 |-  ( G e. USPGraph -> F : ( Walks ` G ) --> ( WWalks ` G ) )
11 simpr 
 |-  ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) -> F : ( Walks ` G ) --> ( WWalks ` G ) )
12 fveq2 
 |-  ( w = x -> ( 2nd ` w ) = ( 2nd ` x ) )
13 id 
 |-  ( x e. ( Walks ` G ) -> x e. ( Walks ` G ) )
14 fvexd 
 |-  ( x e. ( Walks ` G ) -> ( 2nd ` x ) e. _V )
15 1 12 13 14 fvmptd3 
 |-  ( x e. ( Walks ` G ) -> ( F ` x ) = ( 2nd ` x ) )
16 fveq2 
 |-  ( w = y -> ( 2nd ` w ) = ( 2nd ` y ) )
17 id 
 |-  ( y e. ( Walks ` G ) -> y e. ( Walks ` G ) )
18 fvexd 
 |-  ( y e. ( Walks ` G ) -> ( 2nd ` y ) e. _V )
19 1 16 17 18 fvmptd3 
 |-  ( y e. ( Walks ` G ) -> ( F ` y ) = ( 2nd ` y ) )
20 15 19 eqeqan12d 
 |-  ( ( x e. ( Walks ` G ) /\ y e. ( Walks ` G ) ) -> ( ( F ` x ) = ( F ` y ) <-> ( 2nd ` x ) = ( 2nd ` y ) ) )
21 20 adantl 
 |-  ( ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) /\ ( x e. ( Walks ` G ) /\ y e. ( Walks ` G ) ) ) -> ( ( F ` x ) = ( F ` y ) <-> ( 2nd ` x ) = ( 2nd ` y ) ) )
22 uspgr2wlkeqi 
 |-  ( ( G e. USPGraph /\ ( x e. ( Walks ` G ) /\ y e. ( Walks ` G ) ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) -> x = y )
23 22 ad4ant134 
 |-  ( ( ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) /\ ( x e. ( Walks ` G ) /\ y e. ( Walks ` G ) ) ) /\ ( 2nd ` x ) = ( 2nd ` y ) ) -> x = y )
24 23 ex 
 |-  ( ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) /\ ( x e. ( Walks ` G ) /\ y e. ( Walks ` G ) ) ) -> ( ( 2nd ` x ) = ( 2nd ` y ) -> x = y ) )
25 21 24 sylbid 
 |-  ( ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) /\ ( x e. ( Walks ` G ) /\ y e. ( Walks ` G ) ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
26 25 ralrimivva 
 |-  ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) -> A. x e. ( Walks ` G ) A. y e. ( Walks ` G ) ( ( F ` x ) = ( F ` y ) -> x = y ) )
27 dff13 
 |-  ( F : ( Walks ` G ) -1-1-> ( WWalks ` G ) <-> ( F : ( Walks ` G ) --> ( WWalks ` G ) /\ A. x e. ( Walks ` G ) A. y e. ( Walks ` G ) ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
28 11 26 27 sylanbrc 
 |-  ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) -> F : ( Walks ` G ) -1-1-> ( WWalks ` G ) )
29 wlkiswwlks 
 |-  ( G e. USPGraph -> ( E. f f ( Walks ` G ) y <-> y e. ( WWalks ` G ) ) )
30 29 adantr 
 |-  ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) -> ( E. f f ( Walks ` G ) y <-> y e. ( WWalks ` G ) ) )
31 df-br 
 |-  ( f ( Walks ` G ) y <-> <. f , y >. e. ( Walks ` G ) )
32 vex 
 |-  f e. _V
33 vex 
 |-  y e. _V
34 32 33 op2nd 
 |-  ( 2nd ` <. f , y >. ) = y
35 34 eqcomi 
 |-  y = ( 2nd ` <. f , y >. )
36 opex 
 |-  <. f , y >. e. _V
37 eleq1 
 |-  ( x = <. f , y >. -> ( x e. ( Walks ` G ) <-> <. f , y >. e. ( Walks ` G ) ) )
38 fveq2 
 |-  ( x = <. f , y >. -> ( 2nd ` x ) = ( 2nd ` <. f , y >. ) )
39 38 eqeq2d 
 |-  ( x = <. f , y >. -> ( y = ( 2nd ` x ) <-> y = ( 2nd ` <. f , y >. ) ) )
40 37 39 anbi12d 
 |-  ( x = <. f , y >. -> ( ( x e. ( Walks ` G ) /\ y = ( 2nd ` x ) ) <-> ( <. f , y >. e. ( Walks ` G ) /\ y = ( 2nd ` <. f , y >. ) ) ) )
41 36 40 spcev 
 |-  ( ( <. f , y >. e. ( Walks ` G ) /\ y = ( 2nd ` <. f , y >. ) ) -> E. x ( x e. ( Walks ` G ) /\ y = ( 2nd ` x ) ) )
42 35 41 mpan2 
 |-  ( <. f , y >. e. ( Walks ` G ) -> E. x ( x e. ( Walks ` G ) /\ y = ( 2nd ` x ) ) )
43 31 42 sylbi 
 |-  ( f ( Walks ` G ) y -> E. x ( x e. ( Walks ` G ) /\ y = ( 2nd ` x ) ) )
44 43 exlimiv 
 |-  ( E. f f ( Walks ` G ) y -> E. x ( x e. ( Walks ` G ) /\ y = ( 2nd ` x ) ) )
45 30 44 biimtrrdi 
 |-  ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) -> ( y e. ( WWalks ` G ) -> E. x ( x e. ( Walks ` G ) /\ y = ( 2nd ` x ) ) ) )
46 45 imp 
 |-  ( ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) /\ y e. ( WWalks ` G ) ) -> E. x ( x e. ( Walks ` G ) /\ y = ( 2nd ` x ) ) )
47 df-rex 
 |-  ( E. x e. ( Walks ` G ) y = ( 2nd ` x ) <-> E. x ( x e. ( Walks ` G ) /\ y = ( 2nd ` x ) ) )
48 46 47 sylibr 
 |-  ( ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) /\ y e. ( WWalks ` G ) ) -> E. x e. ( Walks ` G ) y = ( 2nd ` x ) )
49 15 eqeq2d 
 |-  ( x e. ( Walks ` G ) -> ( y = ( F ` x ) <-> y = ( 2nd ` x ) ) )
50 49 rexbiia 
 |-  ( E. x e. ( Walks ` G ) y = ( F ` x ) <-> E. x e. ( Walks ` G ) y = ( 2nd ` x ) )
51 48 50 sylibr 
 |-  ( ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) /\ y e. ( WWalks ` G ) ) -> E. x e. ( Walks ` G ) y = ( F ` x ) )
52 51 ralrimiva 
 |-  ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) -> A. y e. ( WWalks ` G ) E. x e. ( Walks ` G ) y = ( F ` x ) )
53 dffo3 
 |-  ( F : ( Walks ` G ) -onto-> ( WWalks ` G ) <-> ( F : ( Walks ` G ) --> ( WWalks ` G ) /\ A. y e. ( WWalks ` G ) E. x e. ( Walks ` G ) y = ( F ` x ) ) )
54 11 52 53 sylanbrc 
 |-  ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) -> F : ( Walks ` G ) -onto-> ( WWalks ` G ) )
55 df-f1o 
 |-  ( F : ( Walks ` G ) -1-1-onto-> ( WWalks ` G ) <-> ( F : ( Walks ` G ) -1-1-> ( WWalks ` G ) /\ F : ( Walks ` G ) -onto-> ( WWalks ` G ) ) )
56 28 54 55 sylanbrc 
 |-  ( ( G e. USPGraph /\ F : ( Walks ` G ) --> ( WWalks ` G ) ) -> F : ( Walks ` G ) -1-1-onto-> ( WWalks ` G ) )
57 10 56 mpdan 
 |-  ( G e. USPGraph -> F : ( Walks ` G ) -1-1-onto-> ( WWalks ` G ) )