Step |
Hyp |
Ref |
Expression |
1 |
|
isclwlk |
|- ( F ( ClWalks ` G ) P <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) ) |
2 |
|
fveq2 |
|- ( ( # ` F ) = 1 -> ( P ` ( # ` F ) ) = ( P ` 1 ) ) |
3 |
2
|
eqeq2d |
|- ( ( # ` F ) = 1 -> ( ( P ` 0 ) = ( P ` ( # ` F ) ) <-> ( P ` 0 ) = ( P ` 1 ) ) ) |
4 |
3
|
anbi2d |
|- ( ( # ` F ) = 1 -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) <-> ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) ) ) |
5 |
|
simp2r |
|- ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> ( P ` 0 ) = ( P ` 1 ) ) |
6 |
|
simp3 |
|- ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> Fun ( iEdg ` G ) ) |
7 |
|
simp2l |
|- ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> F ( Walks ` G ) P ) |
8 |
|
simpr |
|- ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) -> ( P ` 0 ) = ( P ` 1 ) ) |
9 |
8
|
anim2i |
|- ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) |
10 |
9
|
3adant3 |
|- ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) |
11 |
|
wlkl1loop |
|- ( ( ( Fun ( iEdg ` G ) /\ F ( Walks ` G ) P ) /\ ( ( # ` F ) = 1 /\ ( P ` 0 ) = ( P ` 1 ) ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) ) |
12 |
6 7 10 11
|
syl21anc |
|- ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> { ( P ` 0 ) } e. ( Edg ` G ) ) |
13 |
5 12
|
jca |
|- ( ( ( # ` F ) = 1 /\ ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) /\ Fun ( iEdg ` G ) ) -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) ) |
14 |
13
|
3exp |
|- ( ( # ` F ) = 1 -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` 1 ) ) -> ( Fun ( iEdg ` G ) -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) ) ) ) |
15 |
4 14
|
sylbid |
|- ( ( # ` F ) = 1 -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( Fun ( iEdg ` G ) -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) ) ) ) |
16 |
15
|
com13 |
|- ( Fun ( iEdg ` G ) -> ( ( F ( Walks ` G ) P /\ ( P ` 0 ) = ( P ` ( # ` F ) ) ) -> ( ( # ` F ) = 1 -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) ) ) ) |
17 |
1 16
|
syl5bi |
|- ( Fun ( iEdg ` G ) -> ( F ( ClWalks ` G ) P -> ( ( # ` F ) = 1 -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) ) ) ) |
18 |
17
|
3imp |
|- ( ( Fun ( iEdg ` G ) /\ F ( ClWalks ` G ) P /\ ( # ` F ) = 1 ) -> ( ( P ` 0 ) = ( P ` 1 ) /\ { ( P ` 0 ) } e. ( Edg ` G ) ) ) |