Description: Lemma for eupth2 . (Contributed by AV, 25-Feb-2021)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | trlsegvdeg.v | |- V = ( Vtx ` G ) |
|
| trlsegvdeg.i | |- I = ( iEdg ` G ) |
||
| trlsegvdeg.f | |- ( ph -> Fun I ) |
||
| trlsegvdeg.n | |- ( ph -> N e. ( 0 ..^ ( # ` F ) ) ) |
||
| trlsegvdeg.u | |- ( ph -> U e. V ) |
||
| trlsegvdeg.w | |- ( ph -> F ( Trails ` G ) P ) |
||
| trlsegvdeg.vx | |- ( ph -> ( Vtx ` X ) = V ) |
||
| trlsegvdeg.vy | |- ( ph -> ( Vtx ` Y ) = V ) |
||
| trlsegvdeg.vz | |- ( ph -> ( Vtx ` Z ) = V ) |
||
| trlsegvdeg.ix | |- ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) ) |
||
| trlsegvdeg.iy | |- ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) |
||
| trlsegvdeg.iz | |- ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) ) |
||
| eupth2lem3.o | |- ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) |
||
| eupth2lem3.e | |- ( ph -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } ) |
||
| Assertion | eupth2lem3lem5 | |- ( ph -> ( I ` ( F ` N ) ) e. ~P V ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | trlsegvdeg.v | |- V = ( Vtx ` G ) |
|
| 2 | trlsegvdeg.i | |- I = ( iEdg ` G ) |
|
| 3 | trlsegvdeg.f | |- ( ph -> Fun I ) |
|
| 4 | trlsegvdeg.n | |- ( ph -> N e. ( 0 ..^ ( # ` F ) ) ) |
|
| 5 | trlsegvdeg.u | |- ( ph -> U e. V ) |
|
| 6 | trlsegvdeg.w | |- ( ph -> F ( Trails ` G ) P ) |
|
| 7 | trlsegvdeg.vx | |- ( ph -> ( Vtx ` X ) = V ) |
|
| 8 | trlsegvdeg.vy | |- ( ph -> ( Vtx ` Y ) = V ) |
|
| 9 | trlsegvdeg.vz | |- ( ph -> ( Vtx ` Z ) = V ) |
|
| 10 | trlsegvdeg.ix | |- ( ph -> ( iEdg ` X ) = ( I |` ( F " ( 0 ..^ N ) ) ) ) |
|
| 11 | trlsegvdeg.iy | |- ( ph -> ( iEdg ` Y ) = { <. ( F ` N ) , ( I ` ( F ` N ) ) >. } ) |
|
| 12 | trlsegvdeg.iz | |- ( ph -> ( iEdg ` Z ) = ( I |` ( F " ( 0 ... N ) ) ) ) |
|
| 13 | eupth2lem3.o | |- ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` X ) ` x ) } = if ( ( P ` 0 ) = ( P ` N ) , (/) , { ( P ` 0 ) , ( P ` N ) } ) ) |
|
| 14 | eupth2lem3.e | |- ( ph -> ( I ` ( F ` N ) ) = { ( P ` N ) , ( P ` ( N + 1 ) ) } ) |
|
| 15 | 1 2 3 4 5 6 | trlsegvdeglem1 | |- ( ph -> ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) ) |
| 16 | prelpwi | |- ( ( ( P ` N ) e. V /\ ( P ` ( N + 1 ) ) e. V ) -> { ( P ` N ) , ( P ` ( N + 1 ) ) } e. ~P V ) |
|
| 17 | 15 16 | syl | |- ( ph -> { ( P ` N ) , ( P ` ( N + 1 ) ) } e. ~P V ) |
| 18 | 14 17 | eqeltrd | |- ( ph -> ( I ` ( F ` N ) ) e. ~P V ) |