Metamath Proof Explorer

Theorem eupth2

Description: The only vertices of odd degree in a graph with an Eulerian path are the endpoints, and then only if the endpoints are distinct. (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 eupth2 
|- ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) )

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 eqid 
 |-  <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. = <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >.
7 1 2 3 4 5 6 eupthvdres 
 |-  ( ph -> ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) = ( VtxDeg ` G ) )
8 7 fveq1d 
 |-  ( ph -> ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) = ( ( VtxDeg ` G ) ` x ) )
9 8 breq2d 
 |-  ( ph -> ( 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) <-> 2 || ( ( VtxDeg ` G ) ` x ) ) )
10 9 notbid 
 |-  ( ph -> ( -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) <-> -. 2 || ( ( VtxDeg ` G ) ` x ) ) )
11 10 rabbidv 
 |-  ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) } = { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } )
12 eupthiswlk 
 |-  ( F ( EulerPaths ` G ) P -> F ( Walks ` G ) P )
13 wlkcl 
 |-  ( F ( Walks ` G ) P -> ( # ` F ) e. NN0 )
14 5 12 13 3syl 
 |-  ( ph -> ( # ` F ) e. NN0 )
15 nn0re 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) e. RR )
16 15 leidd 
 |-  ( ( # ` F ) e. NN0 -> ( # ` F ) <_ ( # ` F ) )
17 breq1 
 |-  ( m = 0 -> ( m <_ ( # ` F ) <-> 0 <_ ( # ` F ) ) )
18 oveq2 
 |-  ( m = 0 -> ( 0 ..^ m ) = ( 0 ..^ 0 ) )
19 18 imaeq2d 
 |-  ( m = 0 -> ( F " ( 0 ..^ m ) ) = ( F " ( 0 ..^ 0 ) ) )
20 19 reseq2d 
 |-  ( m = 0 -> ( I |` ( F " ( 0 ..^ m ) ) ) = ( I |` ( F " ( 0 ..^ 0 ) ) ) )
21 20 opeq2d 
 |-  ( m = 0 -> <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. = <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. )
22 21 fveq2d 
 |-  ( m = 0 -> ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) = ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. ) )
23 22 fveq1d 
 |-  ( m = 0 -> ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) = ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. ) ` x ) )
24 23 breq2d 
 |-  ( m = 0 -> ( 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) <-> 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. ) ` x ) ) )
25 24 notbid 
 |-  ( m = 0 -> ( -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) <-> -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. ) ` x ) ) )
26 25 rabbidv 
 |-  ( m = 0 -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. ) ` x ) } )
27 fveq2 
 |-  ( m = 0 -> ( P ` m ) = ( P ` 0 ) )
28 27 eqeq2d 
 |-  ( m = 0 -> ( ( P ` 0 ) = ( P ` m ) <-> ( P ` 0 ) = ( P ` 0 ) ) )
29 27 preq2d 
 |-  ( m = 0 -> { ( P ` 0 ) , ( P ` m ) } = { ( P ` 0 ) , ( P ` 0 ) } )
30 28 29 ifbieq2d 
 |-  ( m = 0 -> if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) = if ( ( P ` 0 ) = ( P ` 0 ) , (/) , { ( P ` 0 ) , ( P ` 0 ) } ) )
31 26 30 eqeq12d 
 |-  ( m = 0 -> ( { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) <-> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` 0 ) , (/) , { ( P ` 0 ) , ( P ` 0 ) } ) ) )
32 17 31 imbi12d 
 |-  ( m = 0 -> ( ( m <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) ) <-> ( 0 <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` 0 ) , (/) , { ( P ` 0 ) , ( P ` 0 ) } ) ) ) )
33 32 imbi2d 
 |-  ( m = 0 -> ( ( ph -> ( m <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) ) ) <-> ( ph -> ( 0 <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` 0 ) , (/) , { ( P ` 0 ) , ( P ` 0 ) } ) ) ) ) )
34 breq1 
 |-  ( m = n -> ( m <_ ( # ` F ) <-> n <_ ( # ` F ) ) )
35 oveq2 
 |-  ( m = n -> ( 0 ..^ m ) = ( 0 ..^ n ) )
36 35 imaeq2d 
 |-  ( m = n -> ( F " ( 0 ..^ m ) ) = ( F " ( 0 ..^ n ) ) )
37 36 reseq2d 
 |-  ( m = n -> ( I |` ( F " ( 0 ..^ m ) ) ) = ( I |` ( F " ( 0 ..^ n ) ) ) )
38 37 opeq2d 
 |-  ( m = n -> <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. = <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. )
39 38 fveq2d 
 |-  ( m = n -> ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) = ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) )
40 39 fveq1d 
 |-  ( m = n -> ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) = ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) )
41 40 breq2d 
 |-  ( m = n -> ( 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) <-> 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) ) )
42 41 notbid 
 |-  ( m = n -> ( -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) <-> -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) ) )
43 42 rabbidv 
 |-  ( m = n -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } )
44 fveq2 
 |-  ( m = n -> ( P ` m ) = ( P ` n ) )
45 44 eqeq2d 
 |-  ( m = n -> ( ( P ` 0 ) = ( P ` m ) <-> ( P ` 0 ) = ( P ` n ) ) )
46 44 preq2d 
 |-  ( m = n -> { ( P ` 0 ) , ( P ` m ) } = { ( P ` 0 ) , ( P ` n ) } )
47 45 46 ifbieq2d 
 |-  ( m = n -> if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) )
48 43 47 eqeq12d 
 |-  ( m = n -> ( { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) <-> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) )
49 34 48 imbi12d 
 |-  ( m = n -> ( ( m <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) ) <-> ( n <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) )
50 49 imbi2d 
 |-  ( m = n -> ( ( ph -> ( m <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) ) ) <-> ( ph -> ( n <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) ) )
51 breq1 
 |-  ( m = ( n + 1 ) -> ( m <_ ( # ` F ) <-> ( n + 1 ) <_ ( # ` F ) ) )
52 oveq2 
 |-  ( m = ( n + 1 ) -> ( 0 ..^ m ) = ( 0 ..^ ( n + 1 ) ) )
53 52 imaeq2d 
 |-  ( m = ( n + 1 ) -> ( F " ( 0 ..^ m ) ) = ( F " ( 0 ..^ ( n + 1 ) ) ) )
54 53 reseq2d 
 |-  ( m = ( n + 1 ) -> ( I |` ( F " ( 0 ..^ m ) ) ) = ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) )
55 54 opeq2d 
 |-  ( m = ( n + 1 ) -> <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. = <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. )
56 55 fveq2d 
 |-  ( m = ( n + 1 ) -> ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) = ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) )
57 56 fveq1d 
 |-  ( m = ( n + 1 ) -> ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) = ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) )
58 57 breq2d 
 |-  ( m = ( n + 1 ) -> ( 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) <-> 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) ) )
59 58 notbid 
 |-  ( m = ( n + 1 ) -> ( -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) <-> -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) ) )
60 59 rabbidv 
 |-  ( m = ( n + 1 ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) } )
61 fveq2 
 |-  ( m = ( n + 1 ) -> ( P ` m ) = ( P ` ( n + 1 ) ) )
62 61 eqeq2d 
 |-  ( m = ( n + 1 ) -> ( ( P ` 0 ) = ( P ` m ) <-> ( P ` 0 ) = ( P ` ( n + 1 ) ) ) )
63 61 preq2d 
 |-  ( m = ( n + 1 ) -> { ( P ` 0 ) , ( P ` m ) } = { ( P ` 0 ) , ( P ` ( n + 1 ) ) } )
64 62 63 ifbieq2d 
 |-  ( m = ( n + 1 ) -> if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) = if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) )
65 60 64 eqeq12d 
 |-  ( m = ( n + 1 ) -> ( { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) <-> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( n + 1 ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( n + 1 ) ) , (/) , { ( P ` 0 ) , ( P ` ( n + 1 ) ) } ) ) )
66 51 65 imbi12d 
 |-  ( m = ( n + 1 ) -> ( ( m <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) ) <-> ( ( 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 ) ) } ) ) ) )
67 66 imbi2d 
 |-  ( m = ( n + 1 ) -> ( ( ph -> ( m <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) ) ) <-> ( ph -> ( ( 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 ) ) } ) ) ) ) )
68 breq1 
 |-  ( m = ( # ` F ) -> ( m <_ ( # ` F ) <-> ( # ` F ) <_ ( # ` F ) ) )
69 oveq2 
 |-  ( m = ( # ` F ) -> ( 0 ..^ m ) = ( 0 ..^ ( # ` F ) ) )
70 69 imaeq2d 
 |-  ( m = ( # ` F ) -> ( F " ( 0 ..^ m ) ) = ( F " ( 0 ..^ ( # ` F ) ) ) )
71 70 reseq2d 
 |-  ( m = ( # ` F ) -> ( I |` ( F " ( 0 ..^ m ) ) ) = ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) )
72 71 opeq2d 
 |-  ( m = ( # ` F ) -> <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. = <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. )
73 72 fveq2d 
 |-  ( m = ( # ` F ) -> ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) = ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) )
74 73 fveq1d 
 |-  ( m = ( # ` F ) -> ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) = ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) )
75 74 breq2d 
 |-  ( m = ( # ` F ) -> ( 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) <-> 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) ) )
76 75 notbid 
 |-  ( m = ( # ` F ) -> ( -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) <-> -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) ) )
77 76 rabbidv 
 |-  ( m = ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) } )
78 fveq2 
 |-  ( m = ( # ` F ) -> ( P ` m ) = ( P ` ( # ` F ) ) )
79 78 eqeq2d 
 |-  ( m = ( # ` F ) -> ( ( P ` 0 ) = ( P ` m ) <-> ( P ` 0 ) = ( P ` ( # ` F ) ) ) )
80 78 preq2d 
 |-  ( m = ( # ` F ) -> { ( P ` 0 ) , ( P ` m ) } = { ( P ` 0 ) , ( P ` ( # ` F ) ) } )
81 79 80 ifbieq2d 
 |-  ( m = ( # ` F ) -> if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) )
82 77 81 eqeq12d 
 |-  ( m = ( # ` F ) -> ( { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) <-> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) ) )
83 68 82 imbi12d 
 |-  ( m = ( # ` F ) -> ( ( m <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) ) <-> ( ( # ` F ) <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) ) ) )
84 83 imbi2d 
 |-  ( m = ( # ` F ) -> ( ( ph -> ( m <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ m ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` m ) , (/) , { ( P ` 0 ) , ( P ` m ) } ) ) ) <-> ( ph -> ( ( # ` F ) <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) ) ) ) )
85 1 2 3 4 5 eupth2lemb 
 |-  ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. ) ` x ) } = (/) )
86 eqid 
 |-  ( P ` 0 ) = ( P ` 0 )
87 86 iftruei 
 |-  if ( ( P ` 0 ) = ( P ` 0 ) , (/) , { ( P ` 0 ) , ( P ` 0 ) } ) = (/)
88 85 87 eqtr4di 
 |-  ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` 0 ) , (/) , { ( P ` 0 ) , ( P ` 0 ) } ) )
89 88 a1d 
 |-  ( ph -> ( 0 <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ 0 ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` 0 ) , (/) , { ( P ` 0 ) , ( P ` 0 ) } ) ) )
90 1 2 3 4 5 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 ) ) } ) ) ) )
91 90 expcom 
 |-  ( n e. NN0 -> ( ph -> ( ( 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 ) ) } ) ) ) ) )
92 91 a2d 
 |-  ( n e. NN0 -> ( ( ph -> ( n <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ n ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` n ) , (/) , { ( P ` 0 ) , ( P ` n ) } ) ) ) -> ( ph -> ( ( 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 ) ) } ) ) ) ) )
93 33 50 67 84 89 92 nn0ind 
 |-  ( ( # ` F ) e. NN0 -> ( ph -> ( ( # ` F ) <_ ( # ` F ) -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) ) ) )
94 16 93 mpid 
 |-  ( ( # ` F ) e. NN0 -> ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) ) )
95 14 94 mpcom 
 |-  ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` <. V , ( I |` ( F " ( 0 ..^ ( # ` F ) ) ) ) >. ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) )
96 11 95 eqtr3d 
 |-  ( ph -> { x e. V | -. 2 || ( ( VtxDeg ` G ) ` x ) } = if ( ( P ` 0 ) = ( P ` ( # ` F ) ) , (/) , { ( P ` 0 ) , ( P ` ( # ` F ) ) } ) )