Step |
Hyp |
Ref |
Expression |
1 |
|
prclisacycgr.1 |
|- V = ( Vtx ` G ) |
2 |
|
fvprc |
|- ( -. G e. _V -> ( Vtx ` G ) = (/) ) |
3 |
1 2
|
syl5eq |
|- ( -. G e. _V -> V = (/) ) |
4 |
|
br0 |
|- -. f (/) p |
5 |
|
df-cycls |
|- Cycles = ( g e. _V |-> { <. f , p >. | ( f ( Paths ` g ) p /\ ( p ` 0 ) = ( p ` ( # ` f ) ) ) } ) |
6 |
5
|
relmptopab |
|- Rel ( Cycles ` G ) |
7 |
|
cycliswlk |
|- ( f ( Cycles ` G ) p -> f ( Walks ` G ) p ) |
8 |
|
df-br |
|- ( f ( Cycles ` G ) p <-> <. f , p >. e. ( Cycles ` G ) ) |
9 |
|
df-br |
|- ( f ( Walks ` G ) p <-> <. f , p >. e. ( Walks ` G ) ) |
10 |
7 8 9
|
3imtr3i |
|- ( <. f , p >. e. ( Cycles ` G ) -> <. f , p >. e. ( Walks ` G ) ) |
11 |
6 10
|
relssi |
|- ( Cycles ` G ) C_ ( Walks ` G ) |
12 |
1
|
eqeq1i |
|- ( V = (/) <-> ( Vtx ` G ) = (/) ) |
13 |
|
g0wlk0 |
|- ( ( Vtx ` G ) = (/) -> ( Walks ` G ) = (/) ) |
14 |
12 13
|
sylbi |
|- ( V = (/) -> ( Walks ` G ) = (/) ) |
15 |
11 14
|
sseqtrid |
|- ( V = (/) -> ( Cycles ` G ) C_ (/) ) |
16 |
|
ss0 |
|- ( ( Cycles ` G ) C_ (/) -> ( Cycles ` G ) = (/) ) |
17 |
|
breq |
|- ( ( Cycles ` G ) = (/) -> ( f ( Cycles ` G ) p <-> f (/) p ) ) |
18 |
17
|
notbid |
|- ( ( Cycles ` G ) = (/) -> ( -. f ( Cycles ` G ) p <-> -. f (/) p ) ) |
19 |
15 16 18
|
3syl |
|- ( V = (/) -> ( -. f ( Cycles ` G ) p <-> -. f (/) p ) ) |
20 |
4 19
|
mpbiri |
|- ( V = (/) -> -. f ( Cycles ` G ) p ) |
21 |
20
|
intnanrd |
|- ( V = (/) -> -. ( f ( Cycles ` G ) p /\ f =/= (/) ) ) |
22 |
21
|
nexdv |
|- ( V = (/) -> -. E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) |
23 |
22
|
nexdv |
|- ( V = (/) -> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) |
24 |
3 23
|
syl |
|- ( -. G e. _V -> -. E. f E. p ( f ( Cycles ` G ) p /\ f =/= (/) ) ) |