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 ffvelcdmd 
 |-  ( ( ( 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 bitrid 
 |-  ( ( ( 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 ) ) } ) ) ) )