Metamath Proof Explorer

Theorem upgrimpthslem1

Description: Lemma 1 for upgrimpths . (Contributed by AV, 30-Oct-2025)

Ref Expression
Hypotheses upgrimwlk.i 
|- I = ( iEdg ` G )
upgrimwlk.j 
|- J = ( iEdg ` H )
upgrimwlk.g 
|- ( ph -> G e. USPGraph )
upgrimwlk.h 
|- ( ph -> H e. USPGraph )
upgrimwlk.n 
|- ( ph -> N e. ( G GraphIso H ) )
upgrimwlk.e 
|- E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) )
upgrimpths.p 
|- ( ph -> F ( Paths ` G ) P )
Assertion upgrimpthslem1 
|- ( ph -> Fun `' ( ( N o. P ) |` ( 1 ..^ ( # ` F ) ) ) )

Proof

Step Hyp Ref Expression
1 upgrimwlk.i 
 |-  I = ( iEdg ` G )
2 upgrimwlk.j 
 |-  J = ( iEdg ` H )
3 upgrimwlk.g 
 |-  ( ph -> G e. USPGraph )
4 upgrimwlk.h 
 |-  ( ph -> H e. USPGraph )
5 upgrimwlk.n 
 |-  ( ph -> N e. ( G GraphIso H ) )
6 upgrimwlk.e 
 |-  E = ( x e. dom F |-> ( `' J ` ( N " ( I ` ( F ` x ) ) ) ) )
7 upgrimpths.p 
 |-  ( ph -> F ( Paths ` G ) P )
8 ispth 
 |-  ( F ( Paths ` G ) P <-> ( F ( Trails ` G ) P /\ Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ ( ( P " { 0 , ( # ` F ) } ) i^i ( P " ( 1 ..^ ( # ` F ) ) ) ) = (/) ) )
9 8 simp2bi 
 |-  ( F ( Paths ` G ) P -> Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) )
10 7 9 syl 
 |-  ( ph -> Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) )
11 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
12 eqid 
 |-  ( Vtx ` H ) = ( Vtx ` H )
13 11 12 grimf1o 
 |-  ( N e. ( G GraphIso H ) -> N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) )
14 dff1o3 
 |-  ( N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) <-> ( N : ( Vtx ` G ) -onto-> ( Vtx ` H ) /\ Fun `' N ) )
15 14 simprbi 
 |-  ( N : ( Vtx ` G ) -1-1-onto-> ( Vtx ` H ) -> Fun `' N )
16 5 13 15 3syl 
 |-  ( ph -> Fun `' N )
17 funco 
 |-  ( ( Fun `' ( P |` ( 1 ..^ ( # ` F ) ) ) /\ Fun `' N ) -> Fun ( `' ( P |` ( 1 ..^ ( # ` F ) ) ) o. `' N ) )
18 10 16 17 syl2anc 
 |-  ( ph -> Fun ( `' ( P |` ( 1 ..^ ( # ` F ) ) ) o. `' N ) )
19 resco 
 |-  ( ( N o. P ) |` ( 1 ..^ ( # ` F ) ) ) = ( N o. ( P |` ( 1 ..^ ( # ` F ) ) ) )
20 19 cnveqi 
 |-  `' ( ( N o. P ) |` ( 1 ..^ ( # ` F ) ) ) = `' ( N o. ( P |` ( 1 ..^ ( # ` F ) ) ) )
21 cnvco 
 |-  `' ( N o. ( P |` ( 1 ..^ ( # ` F ) ) ) ) = ( `' ( P |` ( 1 ..^ ( # ` F ) ) ) o. `' N )
22 20 21 eqtri 
 |-  `' ( ( N o. P ) |` ( 1 ..^ ( # ` F ) ) ) = ( `' ( P |` ( 1 ..^ ( # ` F ) ) ) o. `' N )
23 22 funeqi 
 |-  ( Fun `' ( ( N o. P ) |` ( 1 ..^ ( # ` F ) ) ) <-> Fun ( `' ( P |` ( 1 ..^ ( # ` F ) ) ) o. `' N ) )
24 18 23 sylibr 
 |-  ( ph -> Fun `' ( ( N o. P ) |` ( 1 ..^ ( # ` F ) ) ) )