Metamath Proof Explorer

Theorem subgrwlk

Description: If a walk exists in a subgraph of a graph G , then that walk also exists in G . (Contributed by BTernaryTau, 22-Oct-2023)

Ref Expression
Assertion subgrwlk 
|- ( S SubGraph G -> ( F ( Walks ` S ) P -> F ( Walks ` G ) P ) )

Proof

Step Hyp Ref Expression
1 subgrv 
 |-  ( S SubGraph G -> ( S e. _V /\ G e. _V ) )
2 1 simpld 
 |-  ( S SubGraph G -> S e. _V )
3 eqid 
 |-  ( Vtx ` S ) = ( Vtx ` S )
4 eqid 
 |-  ( iEdg ` S ) = ( iEdg ` S )
5 3 4 iswlkg 
 |-  ( S e. _V -> ( F ( Walks ` S ) P <-> ( F e. Word dom ( iEdg ` S ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) ) ) )
6 2 5 syl 
 |-  ( S SubGraph G -> ( F ( Walks ` S ) P <-> ( F e. Word dom ( iEdg ` S ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) ) ) )
7 3simpa 
 |-  ( ( F e. Word dom ( iEdg ` S ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) ) -> ( F e. Word dom ( iEdg ` S ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) ) )
8 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
9 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
10 eqid 
 |-  ( Edg ` S ) = ( Edg ` S )
11 3 8 4 9 10 subgrprop2 
 |-  ( S SubGraph G -> ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) C_ ( iEdg ` G ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) )
12 11 simp2d 
 |-  ( S SubGraph G -> ( iEdg ` S ) C_ ( iEdg ` G ) )
13 dmss 
 |-  ( ( iEdg ` S ) C_ ( iEdg ` G ) -> dom ( iEdg ` S ) C_ dom ( iEdg ` G ) )
14 sswrd 
 |-  ( dom ( iEdg ` S ) C_ dom ( iEdg ` G ) -> Word dom ( iEdg ` S ) C_ Word dom ( iEdg ` G ) )
15 12 13 14 3syl 
 |-  ( S SubGraph G -> Word dom ( iEdg ` S ) C_ Word dom ( iEdg ` G ) )
16 15 sseld 
 |-  ( S SubGraph G -> ( F e. Word dom ( iEdg ` S ) -> F e. Word dom ( iEdg ` G ) ) )
17 11 simp1d 
 |-  ( S SubGraph G -> ( Vtx ` S ) C_ ( Vtx ` G ) )
18 fss 
 |-  ( ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) /\ ( Vtx ` S ) C_ ( Vtx ` G ) ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
19 18 expcom 
 |-  ( ( Vtx ` S ) C_ ( Vtx ` G ) -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) )
20 17 19 syl 
 |-  ( S SubGraph G -> ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) )
21 16 20 anim12d 
 |-  ( S SubGraph G -> ( ( F e. Word dom ( iEdg ` S ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) ) -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) ) )
22 7 21 syl5 
 |-  ( S SubGraph G -> ( ( F e. Word dom ( iEdg ` S ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) ) -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) ) )
23 3simpb 
 |-  ( ( F e. Word dom ( iEdg ` S ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) ) -> ( F e. Word dom ( iEdg ` S ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) ) )
24 3 8 4 9 10 subgrprop 
 |-  ( S SubGraph G -> ( ( Vtx ` S ) C_ ( Vtx ` G ) /\ ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) /\ ( Edg ` S ) C_ ~P ( Vtx ` S ) ) )
25 24 simp2d 
 |-  ( S SubGraph G -> ( iEdg ` S ) = ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) )
26 25 fveq1d 
 |-  ( S SubGraph G -> ( ( iEdg ` S ) ` ( F ` k ) ) = ( ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) ` ( F ` k ) ) )
27 26 3ad2ant1 
 |-  ( ( S SubGraph G /\ F e. Word dom ( iEdg ` S ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` S ) ` ( F ` k ) ) = ( ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) ` ( F ` k ) ) )
28 wrdsymbcl 
 |-  ( ( F e. Word dom ( iEdg ` S ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( F ` k ) e. dom ( iEdg ` S ) )
29 28 fvresd 
 |-  ( ( F e. Word dom ( iEdg ` S ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( F ` k ) ) )
30 29 3adant1 
 |-  ( ( S SubGraph G /\ F e. Word dom ( iEdg ` S ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( iEdg ` G ) |` dom ( iEdg ` S ) ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( F ` k ) ) )
31 27 30 eqtrd 
 |-  ( ( S SubGraph G /\ F e. Word dom ( iEdg ` S ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( iEdg ` S ) ` ( F ` k ) ) = ( ( iEdg ` G ) ` ( F ` k ) ) )
32 31 eqeq1d 
 |-  ( ( S SubGraph G /\ F e. Word dom ( iEdg ` S ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } <-> ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } ) )
33 31 sseq2d 
 |-  ( ( S SubGraph G /\ F e. Word dom ( iEdg ` S ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) <-> { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) )
34 32 33 ifpbi23d 
 |-  ( ( S SubGraph G /\ F e. Word dom ( iEdg ` S ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) <-> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
35 34 biimpd 
 |-  ( ( S SubGraph G /\ F e. Word dom ( iEdg ` S ) /\ k e. ( 0 ..^ ( # ` F ) ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) -> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
36 35 3expia 
 |-  ( ( S SubGraph G /\ F e. Word dom ( iEdg ` S ) ) -> ( k e. ( 0 ..^ ( # ` F ) ) -> ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) -> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
37 36 ralrimiv 
 |-  ( ( S SubGraph G /\ F e. Word dom ( iEdg ` S ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) -> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
38 ralim 
 |-  ( A. k e. ( 0 ..^ ( # ` F ) ) ( if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) -> if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
39 37 38 syl 
 |-  ( ( S SubGraph G /\ F e. Word dom ( iEdg ` S ) ) -> ( A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
40 39 expimpd 
 |-  ( S SubGraph G -> ( ( F e. Word dom ( iEdg ` S ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
41 23 40 syl5 
 |-  ( S SubGraph G -> ( ( F e. Word dom ( iEdg ` S ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) ) -> A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
42 22 41 jcad 
 |-  ( S SubGraph G -> ( ( F e. Word dom ( iEdg ` S ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` S ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` S ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` S ) ` ( F ` k ) ) ) ) -> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
43 6 42 sylbid 
 |-  ( S SubGraph G -> ( F ( Walks ` S ) P -> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
44 df-3an 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) <-> ( ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) )
45 43 44 imbitrrdi 
 |-  ( S SubGraph G -> ( F ( Walks ` S ) P -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
46 8 9 iswlkg 
 |-  ( G e. _V -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
47 1 46 simpl2im 
 |-  ( S SubGraph G -> ( F ( Walks ` G ) P <-> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) /\ A. k e. ( 0 ..^ ( # ` F ) ) if- ( ( P ` k ) = ( P ` ( k + 1 ) ) , ( ( iEdg ` G ) ` ( F ` k ) ) = { ( P ` k ) } , { ( P ` k ) , ( P ` ( k + 1 ) ) } C_ ( ( iEdg ` G ) ` ( F ` k ) ) ) ) ) )
48 45 47 sylibrd 
 |-  ( S SubGraph G -> ( F ( Walks ` S ) P -> F ( Walks ` G ) P ) )