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 ) ) } ) ) ) ) |