This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem wlkp1lem4

Description: Lemma for wlkp1 . (Contributed by AV, 6-Mar-2021)

Ref Expression
Hypotheses wlkp1.v 
|- V = ( Vtx ` G )
wlkp1.i 
|- I = ( iEdg ` G )
wlkp1.f 
|- ( ph -> Fun I )
wlkp1.a 
|- ( ph -> I e. Fin )
wlkp1.b 
|- ( ph -> B e. W )
wlkp1.c 
|- ( ph -> C e. V )
wlkp1.d 
|- ( ph -> -. B e. dom I )
wlkp1.w 
|- ( ph -> F ( Walks ` G ) P )
wlkp1.n 
|- N = ( # ` F )
wlkp1.e 
|- ( ph -> E e. ( Edg ` G ) )
wlkp1.x 
|- ( ph -> { ( P ` N ) , C } C_ E )
wlkp1.u 
|- ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
wlkp1.h 
|- H = ( F u. { <. N , B >. } )
wlkp1.q 
|- Q = ( P u. { <. ( N + 1 ) , C >. } )
wlkp1.s 
|- ( ph -> ( Vtx ` S ) = V )
Assertion wlkp1lem4 
|- ( ph -> ( S e. _V /\ H e. _V /\ Q e. _V ) )

Proof

Step Hyp Ref Expression
1 wlkp1.v 
 |-  V = ( Vtx ` G )
2 wlkp1.i 
 |-  I = ( iEdg ` G )
3 wlkp1.f 
 |-  ( ph -> Fun I )
4 wlkp1.a 
 |-  ( ph -> I e. Fin )
5 wlkp1.b 
 |-  ( ph -> B e. W )
6 wlkp1.c 
 |-  ( ph -> C e. V )
7 wlkp1.d 
 |-  ( ph -> -. B e. dom I )
8 wlkp1.w 
 |-  ( ph -> F ( Walks ` G ) P )
9 wlkp1.n 
 |-  N = ( # ` F )
10 wlkp1.e 
 |-  ( ph -> E e. ( Edg ` G ) )
11 wlkp1.x 
 |-  ( ph -> { ( P ` N ) , C } C_ E )
12 wlkp1.u 
 |-  ( ph -> ( iEdg ` S ) = ( I u. { <. B , E >. } ) )
13 wlkp1.h 
 |-  H = ( F u. { <. N , B >. } )
14 wlkp1.q 
 |-  Q = ( P u. { <. ( N + 1 ) , C >. } )
15 wlkp1.s 
 |-  ( ph -> ( Vtx ` S ) = V )
16 eqid 
 |-  ( iEdg ` G ) = ( iEdg ` G )
17 16 wlkf 
 |-  ( F ( Walks ` G ) P -> F e. Word dom ( iEdg ` G ) )
18 eqid 
 |-  ( Vtx ` G ) = ( Vtx ` G )
19 18 wlkp 
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) )
20 17 19 jca 
 |-  ( F ( Walks ` G ) P -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) )
21 8 20 syl 
 |-  ( ph -> ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) )
22 6 15 eleqtrrd 
 |-  ( ph -> C e. ( Vtx ` S ) )
23 22 elfvexd 
 |-  ( ph -> S e. _V )
24 23 adantr 
 |-  ( ( ph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) ) -> S e. _V )
25 simprl 
 |-  ( ( ph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) ) -> F e. Word dom ( iEdg ` G ) )
26 snex 
 |-  { <. N , B >. } e. _V
27 unexg 
 |-  ( ( F e. Word dom ( iEdg ` G ) /\ { <. N , B >. } e. _V ) -> ( F u. { <. N , B >. } ) e. _V )
28 25 26 27 sylancl 
 |-  ( ( ph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) ) -> ( F u. { <. N , B >. } ) e. _V )
29 13 28 eqeltrid 
 |-  ( ( ph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) ) -> H e. _V )
30 ovex 
 |-  ( 0 ... ( # ` F ) ) e. _V
31 fvex 
 |-  ( Vtx ` G ) e. _V
32 30 31 fpm 
 |-  ( P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) -> P e. ( ( Vtx ` G ) ^pm ( 0 ... ( # ` F ) ) ) )
33 32 ad2antll 
 |-  ( ( ph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) ) -> P e. ( ( Vtx ` G ) ^pm ( 0 ... ( # ` F ) ) ) )
34 snex 
 |-  { <. ( N + 1 ) , C >. } e. _V
35 unexg 
 |-  ( ( P e. ( ( Vtx ` G ) ^pm ( 0 ... ( # ` F ) ) ) /\ { <. ( N + 1 ) , C >. } e. _V ) -> ( P u. { <. ( N + 1 ) , C >. } ) e. _V )
36 33 34 35 sylancl 
 |-  ( ( ph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) ) -> ( P u. { <. ( N + 1 ) , C >. } ) e. _V )
37 14 36 eqeltrid 
 |-  ( ( ph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) ) -> Q e. _V )
38 24 29 37 3jca 
 |-  ( ( ph /\ ( F e. Word dom ( iEdg ` G ) /\ P : ( 0 ... ( # ` F ) ) --> ( Vtx ` G ) ) ) -> ( S e. _V /\ H e. _V /\ Q e. _V ) )
39 21 38 mpdan 
 |-  ( ph -> ( S e. _V /\ H e. _V /\ Q e. _V ) )