Metamath Proof Explorer

Theorem clwwlkfo

Description: Lemma 4 for clwwlkf1o : F is an onto function. (Contributed by Alexander van der Vekens, 29-Sep-2018) (Revised by AV, 26-Apr-2021) (Revised by AV, 1-Nov-2022)

Ref Expression
Hypotheses clwwlkf1o.d 
|- D = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) }
clwwlkf1o.f 
|- F = ( t e. D |-> ( t prefix N ) )
Assertion clwwlkfo 
|- ( N e. NN -> F : D -onto-> ( N ClWWalksN G ) )

Proof

Step Hyp Ref Expression
1 clwwlkf1o.d 
 |-  D = { w e. ( N WWalksN G ) | ( lastS ` w ) = ( w ` 0 ) }
2 clwwlkf1o.f 
 |-  F = ( t e. D |-> ( t prefix N ) )
3 1 2 clwwlkf 
 |-  ( N e. NN -> F : D --> ( N ClWWalksN G ) )
4 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
5 eqid 
 |-  ( Edg ` G ) = ( Edg ` G )
6 4 5 clwwlknp 
 |-  ( p e. ( N ClWWalksN G ) -> ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) )
7 simpr 
 |-  ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> N e. NN )
8 simpl1 
 |-  ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) )
9 3simpc 
 |-  ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) )
10 9 adantr 
 |-  ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) )
11 1 clwwlkel 
 |-  ( ( N e. NN /\ ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ ( A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) ) -> ( p ++ <" ( p ` 0 ) "> ) e. D )
12 7 8 10 11 syl3anc 
 |-  ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( p ++ <" ( p ` 0 ) "> ) e. D )
13 oveq2 
 |-  ( N = ( # ` p ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) )
14 13 eqcoms 
 |-  ( ( # ` p ) = N -> ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) )
15 14 adantl 
 |-  ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) )
16 15 3ad2ant1 
 |-  ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) )
17 16 adantr 
 |-  ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) )
18 simpll 
 |-  ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ N e. NN ) -> p e. Word ( Vtx ` G ) )
19 fstwrdne0 
 |-  ( ( N e. NN /\ ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) ) -> ( p ` 0 ) e. ( Vtx ` G ) )
20 19 ancoms 
 |-  ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ N e. NN ) -> ( p ` 0 ) e. ( Vtx ` G ) )
21 20 s1cld 
 |-  ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ N e. NN ) -> <" ( p ` 0 ) "> e. Word ( Vtx ` G ) )
22 18 21 jca 
 |-  ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ N e. NN ) -> ( p e. Word ( Vtx ` G ) /\ <" ( p ` 0 ) "> e. Word ( Vtx ` G ) ) )
23 22 3ad2antl1 
 |-  ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( p e. Word ( Vtx ` G ) /\ <" ( p ` 0 ) "> e. Word ( Vtx ` G ) ) )
24 pfxccat1 
 |-  ( ( p e. Word ( Vtx ` G ) /\ <" ( p ` 0 ) "> e. Word ( Vtx ` G ) ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) = p )
25 23 24 syl 
 |-  ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( ( p ++ <" ( p ` 0 ) "> ) prefix ( # ` p ) ) = p )
26 17 25 eqtr2d 
 |-  ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) )
27 12 26 jca 
 |-  ( ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) /\ N e. NN ) -> ( ( p ++ <" ( p ` 0 ) "> ) e. D /\ p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) )
28 27 ex 
 |-  ( ( ( p e. Word ( Vtx ` G ) /\ ( # ` p ) = N ) /\ A. i e. ( 0 ..^ ( N - 1 ) ) { ( p ` i ) , ( p ` ( i + 1 ) ) } e. ( Edg ` G ) /\ { ( lastS ` p ) , ( p ` 0 ) } e. ( Edg ` G ) ) -> ( N e. NN -> ( ( p ++ <" ( p ` 0 ) "> ) e. D /\ p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) ) )
29 6 28 syl 
 |-  ( p e. ( N ClWWalksN G ) -> ( N e. NN -> ( ( p ++ <" ( p ` 0 ) "> ) e. D /\ p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) ) )
30 29 impcom 
 |-  ( ( N e. NN /\ p e. ( N ClWWalksN G ) ) -> ( ( p ++ <" ( p ` 0 ) "> ) e. D /\ p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) )
31 oveq1 
 |-  ( x = ( p ++ <" ( p ` 0 ) "> ) -> ( x prefix N ) = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) )
32 31 rspceeqv 
 |-  ( ( ( p ++ <" ( p ` 0 ) "> ) e. D /\ p = ( ( p ++ <" ( p ` 0 ) "> ) prefix N ) ) -> E. x e. D p = ( x prefix N ) )
33 30 32 syl 
 |-  ( ( N e. NN /\ p e. ( N ClWWalksN G ) ) -> E. x e. D p = ( x prefix N ) )
34 1 2 clwwlkfv 
 |-  ( x e. D -> ( F ` x ) = ( x prefix N ) )
35 34 eqeq2d 
 |-  ( x e. D -> ( p = ( F ` x ) <-> p = ( x prefix N ) ) )
36 35 adantl 
 |-  ( ( ( N e. NN /\ p e. ( N ClWWalksN G ) ) /\ x e. D ) -> ( p = ( F ` x ) <-> p = ( x prefix N ) ) )
37 36 rexbidva 
 |-  ( ( N e. NN /\ p e. ( N ClWWalksN G ) ) -> ( E. x e. D p = ( F ` x ) <-> E. x e. D p = ( x prefix N ) ) )
38 33 37 mpbird 
 |-  ( ( N e. NN /\ p e. ( N ClWWalksN G ) ) -> E. x e. D p = ( F ` x ) )
39 38 ralrimiva 
 |-  ( N e. NN -> A. p e. ( N ClWWalksN G ) E. x e. D p = ( F ` x ) )
40 dffo3 
 |-  ( F : D -onto-> ( N ClWWalksN G ) <-> ( F : D --> ( N ClWWalksN G ) /\ A. p e. ( N ClWWalksN G ) E. x e. D p = ( F ` x ) ) )
41 3 39 40 sylanbrc 
 |-  ( N e. NN -> F : D -onto-> ( N ClWWalksN G ) )