Metamath Proof Explorer


Theorem eupth2lems

Description: Lemma for eupth2 (induction step): The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct, if the Eulerian path shortened by one edge has this property. Formerly part of proof for eupth2 . (Contributed by Mario Carneiro, 8-Apr-2015) (Revised by AV, 26-Feb-2021)

Ref Expression
Hypotheses eupth2.v
|- V = ( Vtx ` G )
eupth2.i
|- I = ( iEdg ` G )
eupth2.g
|- ( ph -> G e. UPGraph )
eupth2.f
|- ( ph -> Fun I )
eupth2.p
|- ( ph -> F ( EulerPaths ` G ) P )
Assertion eupth2lems
|- ( ( ph /\ n e. NN0 ) -> ( ( n <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) -> ( ( n + 1 ) <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 eupth2.v
 |-  V = ( Vtx ` G )
2 eupth2.i
 |-  I = ( iEdg ` G )
3 eupth2.g
 |-  ( ph -> G e. UPGraph )
4 eupth2.f
 |-  ( ph -> Fun I )
5 eupth2.p
 |-  ( ph -> F ( EulerPaths ` G ) P )
6 nn0re
 |-  ( n e. NN0 -> n e. RR )
7 6 adantl
 |-  ( ( ph /\ n e. NN0 ) -> n e. RR )
8 7 lep1d
 |-  ( ( ph /\ n e. NN0 ) -> n <_ ( n + 1 ) )
9 peano2re
 |-  ( n e. RR -> ( n + 1 ) e. RR )
10 7 9 syl
 |-  ( ( ph /\ n e. NN0 ) -> ( n + 1 ) e. RR )
11 eupthiswlk
 |-  ( F ( EulerPaths ` G ) P -> F ( Walks ` G ) P )
12 wlkcl
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
13 5 11 12 3syl
 |-  ( ph -> ( # ` F ) e. NN0 )
14 13 nn0red
 |-  ( ph -> ( # ` F ) e. RR )
15 14 adantr
 |-  ( ( ph /\ n e. NN0 ) -> ( # ` F ) e. RR )
16 letr
 |-  ( ( n e. RR /\ ( n + 1 ) e. RR /\ ( # ` F ) e. RR ) -> ( ( n <_ ( n + 1 ) /\ ( n + 1 ) <_ ( # ` F ) ) -> n <_ ( # ` F ) ) )
17 7 10 15 16 syl3anc
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n <_ ( n + 1 ) /\ ( n + 1 ) <_ ( # ` F ) ) -> n <_ ( # ` F ) ) )
18 8 17 mpand
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n + 1 ) <_ ( # ` F ) -> n <_ ( # ` F ) ) )
19 18 imim1d
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) -> ( ( n + 1 ) <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) )
20 fveq2
 |-  ( x = y -> ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) = ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` y ) )
21 20 breq2d
 |-  ( x = y -> ( 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) <-> 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` y ) ) )
22 21 notbid
 |-  ( x = y -> ( -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) <-> -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` y ) ) )
23 22 elrab
 |-  ( y e. { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) } <-> ( y e. V /\ -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` y ) ) )
24 3 ad3antrrr
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) /\ y e. V ) -> G e. UPGraph )
25 4 ad3antrrr
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) /\ y e. V ) -> Fun I )
26 5 ad3antrrr
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) /\ y e. V ) -> F ( EulerPaths ` G ) P )
27 eqid
 |-  <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. = <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >.
28 eqid
 |-  <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. = <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >.
29 simpr
 |-  ( ( ph /\ n e. NN0 ) -> n e. NN0 )
30 29 ad2antrr
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) /\ y e. V ) -> n e. NN0 )
31 simprl
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( n + 1 ) <_ ( # ` F ) )
32 31 adantr
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) /\ y e. V ) -> ( n + 1 ) <_ ( # ` F ) )
33 simpr
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) /\ y e. V ) -> y e. V )
34 simplrr
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) /\ y e. V ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) )
35 1 2 24 25 26 27 28 30 32 33 34 eupth2lem3
 |-  ( ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) /\ y e. V ) -> ( -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` y ) <-> y e. if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) ) )
36 35 pm5.32da
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( ( y e. V /\ -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` y ) ) <-> ( y e. V /\ y e. if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) ) ) )
37 0elpw
 |-  (/) e. ~P V
38 1 wlkepvtx
 |-  ( F ( Walks ` G ) P -> ( ( P ` 0 ) e. V /\ ( P ` ( # ` F ) ) e. V ) )
39 38 simpld
 |-  ( F ( Walks ` G ) P -> ( P ` 0 ) e. V )
40 5 11 39 3syl
 |-  ( ph -> ( P ` 0 ) e. V )
41 40 ad2antrr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( P ` 0 ) e. V )
42 1 wlkp
 |-  ( F ( Walks ` G ) P -> P : ( 0 ... ( # ` F ) ) --> V )
43 5 11 42 3syl
 |-  ( ph -> P : ( 0 ... ( # ` F ) ) --> V )
44 43 ad2antrr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> P : ( 0 ... ( # ` F ) ) --> V )
45 peano2nn0
 |-  ( n e. NN0 -> ( n + 1 ) e. NN0 )
46 45 adantl
 |-  ( ( ph /\ n e. NN0 ) -> ( n + 1 ) e. NN0 )
47 46 adantr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( n + 1 ) e. NN0 )
48 nn0uz
 |-  NN0 = ( ZZ>= ` 0 )
49 47 48 eleqtrdi
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( n + 1 ) e. ( ZZ>= ` 0 ) )
50 13 ad2antrr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( # ` F ) e. NN0 )
51 50 nn0zd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( # ` F ) e. ZZ )
52 elfz5
 |-  ( ( ( n + 1 ) e. ( ZZ>= ` 0 ) /\ ( # ` F ) e. ZZ ) -> ( ( n + 1 ) e. ( 0 ... ( # ` F ) ) <-> ( n + 1 ) <_ ( # ` F ) ) )
53 49 51 52 syl2anc
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( ( n + 1 ) e. ( 0 ... ( # ` F ) ) <-> ( n + 1 ) <_ ( # ` F ) ) )
54 31 53 mpbird
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( n + 1 ) e. ( 0 ... ( # ` F ) ) )
55 44 54 ffvelrnd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( P ` ( n + 1 ) ) e. V )
56 41 55 prssd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> { ( P ` 0 ) , ( P ` ( n + 1 ) ) } C_ V )
57 prex
 |-  { ( P ` 0 ) , ( P ` ( n + 1 ) ) } e. _V
58 57 elpw
 |-  ( { ( P ` 0 ) , ( P ` ( n + 1 ) ) } e. ~P V <-> { ( P ` 0 ) , ( P ` ( n + 1 ) ) } C_ V )
59 56 58 sylibr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> { ( P ` 0 ) , ( P ` ( n + 1 ) ) } e. ~P V )
60 ifcl
 |-  ( ( (/) e. ~P V /\ { ( P ` 0 ) , ( P ` ( n + 1 ) ) } e. ~P V ) -> if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) e. ~P V )
61 37 59 60 sylancr
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) e. ~P V )
62 61 elpwid
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) C_ V )
63 62 sseld
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( y e. if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) -> y e. V ) )
64 63 pm4.71rd
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( y e. if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) <-> ( y e. V /\ y e. if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) ) ) )
65 36 64 bitr4d
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( ( y e. V /\ -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` y ) ) <-> y e. if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) ) )
66 23 65 syl5bb
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( y e. { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) } <-> y e. if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) ) )
67 66 eqrdv
 |-  ( ( ( ph /\ n e. NN0 ) /\ ( ( n + 1 ) <_ ( # ` F ) /\ { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) )
68 67 exp32
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n + 1 ) <_ ( # ` F ) -> ( { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) ) ) )
69 68 a2d
 |-  ( ( ph /\ n e. NN0 ) -> ( ( ( n + 1 ) <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) -> ( ( n + 1 ) <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) ) ) )
70 19 69 syld
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) -> ( ( n + 1 ) <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) ) ) )