Metamath Proof Explorer

Theorem wlkreslem

Description: Lemma for wlkres . (Contributed by AV, 5-Mar-2021) (Revised by AV, 30-Nov-2022)

Ref Expression
Hypotheses wlkres.v 
|- V = ( Vtx ` G )
wlkres.i 
|- I = ( iEdg ` G )
wlkres.d 
|- ( ph -> F ( Walks ` G ) P )
wlkres.n 
|- ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
wlkres.s 
|- ( ph -> ( Vtx ` S ) = V )
Assertion wlkreslem 
|- ( ph -> S e. _V )

Proof

Step Hyp Ref Expression
1 wlkres.v 
 |-  V = ( Vtx ` G )
2 wlkres.i 
 |-  I = ( iEdg ` G )
3 wlkres.d 
 |-  ( ph -> F ( Walks ` G ) P )
4 wlkres.n 
 |-  ( ph -> N e. ( 0 ..^ ( # ` F ) ) )
5 wlkres.s 
 |-  ( ph -> ( Vtx ` S ) = V )
6 ax-1 
 |-  ( S e. _V -> ( ph -> S e. _V ) )
7 df-nel 
 |-  ( S e/ _V <-> -. S e. _V )
8 df-br 
 |-  ( F ( Walks ` G ) P <-> <. F , P >. e. ( Walks ` G ) )
9 ne0i 
 |-  ( <. F , P >. e. ( Walks ` G ) -> ( Walks ` G ) =/= (/) )
10 5 1 eqtrdi 
 |-  ( ph -> ( Vtx ` S ) = ( Vtx ` G ) )
11 10 anim1ci 
 |-  ( ( ph /\ S e/ _V ) -> ( S e/ _V /\ ( Vtx ` S ) = ( Vtx ` G ) ) )
12 wlk0prc 
 |-  ( ( S e/ _V /\ ( Vtx ` S ) = ( Vtx ` G ) ) -> ( Walks ` G ) = (/) )
13 eqneqall 
 |-  ( ( Walks ` G ) = (/) -> ( ( Walks ` G ) =/= (/) -> S e. _V ) )
14 11 12 13 3syl 
 |-  ( ( ph /\ S e/ _V ) -> ( ( Walks ` G ) =/= (/) -> S e. _V ) )
15 14 expcom 
 |-  ( S e/ _V -> ( ph -> ( ( Walks ` G ) =/= (/) -> S e. _V ) ) )
16 15 com13 
 |-  ( ( Walks ` G ) =/= (/) -> ( ph -> ( S e/ _V -> S e. _V ) ) )
17 9 16 syl 
 |-  ( <. F , P >. e. ( Walks ` G ) -> ( ph -> ( S e/ _V -> S e. _V ) ) )
18 8 17 sylbi 
 |-  ( F ( Walks ` G ) P -> ( ph -> ( S e/ _V -> S e. _V ) ) )
19 3 18 mpcom 
 |-  ( ph -> ( S e/ _V -> S e. _V ) )
20 19 com12 
 |-  ( S e/ _V -> ( ph -> S e. _V ) )
21 7 20 sylbir 
 |-  ( -. S e. _V -> ( ph -> S e. _V ) )
22 6 21 pm2.61i 
 |-  ( ph -> S e. _V )