Metamath Proof Explorer

Theorem clwlkclwwlkfolem

Description: Lemma for clwlkclwwlkfo . (Contributed by AV, 25-May-2022)

Ref Expression
Hypothesis clwlkclwwlkf.c 
|- C = { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) }
Assertion clwlkclwwlkfolem 
|- ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) /\ <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. C )

Proof

Step Hyp Ref Expression
1 clwlkclwwlkf.c 
 |-  C = { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) }
2 simp3 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) /\ <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. ( ClWalks ` G ) )
3 wrdlenccats1lenm1 
 |-  ( W e. Word ( Vtx ` G ) -> ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) = ( # ` W ) )
4 3 eqcomd 
 |-  ( W e. Word ( Vtx ` G ) -> ( # ` W ) = ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) )
5 4 breq2d 
 |-  ( W e. Word ( Vtx ` G ) -> ( 1 <_ ( # ` W ) <-> 1 <_ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) ) )
6 5 biimpa 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) ) -> 1 <_ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) )
7 6 3adant3 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) /\ <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> 1 <_ ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) )
8 df-br 
 |-  ( f ( ClWalks ` G ) ( W ++ <" ( W ` 0 ) "> ) <-> <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. ( ClWalks ` G ) )
9 clwlkiswlk 
 |-  ( f ( ClWalks ` G ) ( W ++ <" ( W ` 0 ) "> ) -> f ( Walks ` G ) ( W ++ <" ( W ` 0 ) "> ) )
10 wlklenvm1 
 |-  ( f ( Walks ` G ) ( W ++ <" ( W ` 0 ) "> ) -> ( # ` f ) = ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) )
11 9 10 syl 
 |-  ( f ( ClWalks ` G ) ( W ++ <" ( W ` 0 ) "> ) -> ( # ` f ) = ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) )
12 8 11 sylbir 
 |-  ( <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. ( ClWalks ` G ) -> ( # ` f ) = ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) )
13 12 3ad2ant3 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) /\ <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> ( # ` f ) = ( ( # ` ( W ++ <" ( W ` 0 ) "> ) ) - 1 ) )
14 7 13 breqtrrd 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) /\ <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> 1 <_ ( # ` f ) )
15 vex 
 |-  f e. _V
16 ovex 
 |-  ( W ++ <" ( W ` 0 ) "> ) e. _V
17 15 16 op1std 
 |-  ( c = <. f , ( W ++ <" ( W ` 0 ) "> ) >. -> ( 1st ` c ) = f )
18 17 fveq2d 
 |-  ( c = <. f , ( W ++ <" ( W ` 0 ) "> ) >. -> ( # ` ( 1st ` c ) ) = ( # ` f ) )
19 18 breq2d 
 |-  ( c = <. f , ( W ++ <" ( W ` 0 ) "> ) >. -> ( 1 <_ ( # ` ( 1st ` c ) ) <-> 1 <_ ( # ` f ) ) )
20 2fveq3 
 |-  ( w = c -> ( # ` ( 1st ` w ) ) = ( # ` ( 1st ` c ) ) )
21 20 breq2d 
 |-  ( w = c -> ( 1 <_ ( # ` ( 1st ` w ) ) <-> 1 <_ ( # ` ( 1st ` c ) ) ) )
22 21 cbvrabv 
 |-  { w e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` w ) ) } = { c e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` c ) ) }
23 1 22 eqtri 
 |-  C = { c e. ( ClWalks ` G ) | 1 <_ ( # ` ( 1st ` c ) ) }
24 19 23 elrab2 
 |-  ( <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. C <-> ( <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. ( ClWalks ` G ) /\ 1 <_ ( # ` f ) ) )
25 2 14 24 sylanbrc 
 |-  ( ( W e. Word ( Vtx ` G ) /\ 1 <_ ( # ` W ) /\ <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. ( ClWalks ` G ) ) -> <. f , ( W ++ <" ( W ` 0 ) "> ) >. e. C )