Step |
Hyp |
Ref |
Expression |
1 |
|
1loopgruspgr.v |
|- ( ph -> ( Vtx ` G ) = V ) |
2 |
|
1loopgruspgr.a |
|- ( ph -> A e. X ) |
3 |
|
1loopgruspgr.n |
|- ( ph -> N e. V ) |
4 |
|
1loopgruspgr.i |
|- ( ph -> ( iEdg ` G ) = { <. A , { N } >. } ) |
5 |
|
1loopgrvd0.k |
|- ( ph -> K e. ( V \ { N } ) ) |
6 |
5
|
eldifbd |
|- ( ph -> -. K e. { N } ) |
7 |
|
snex |
|- { N } e. _V |
8 |
|
fvsng |
|- ( ( A e. X /\ { N } e. _V ) -> ( { <. A , { N } >. } ` A ) = { N } ) |
9 |
2 7 8
|
sylancl |
|- ( ph -> ( { <. A , { N } >. } ` A ) = { N } ) |
10 |
9
|
eleq2d |
|- ( ph -> ( K e. ( { <. A , { N } >. } ` A ) <-> K e. { N } ) ) |
11 |
6 10
|
mtbird |
|- ( ph -> -. K e. ( { <. A , { N } >. } ` A ) ) |
12 |
4
|
dmeqd |
|- ( ph -> dom ( iEdg ` G ) = dom { <. A , { N } >. } ) |
13 |
|
dmsnopg |
|- ( { N } e. _V -> dom { <. A , { N } >. } = { A } ) |
14 |
7 13
|
mp1i |
|- ( ph -> dom { <. A , { N } >. } = { A } ) |
15 |
12 14
|
eqtrd |
|- ( ph -> dom ( iEdg ` G ) = { A } ) |
16 |
4
|
fveq1d |
|- ( ph -> ( ( iEdg ` G ) ` i ) = ( { <. A , { N } >. } ` i ) ) |
17 |
16
|
eleq2d |
|- ( ph -> ( K e. ( ( iEdg ` G ) ` i ) <-> K e. ( { <. A , { N } >. } ` i ) ) ) |
18 |
15 17
|
rexeqbidv |
|- ( ph -> ( E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) <-> E. i e. { A } K e. ( { <. A , { N } >. } ` i ) ) ) |
19 |
|
fveq2 |
|- ( i = A -> ( { <. A , { N } >. } ` i ) = ( { <. A , { N } >. } ` A ) ) |
20 |
19
|
eleq2d |
|- ( i = A -> ( K e. ( { <. A , { N } >. } ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) ) |
21 |
20
|
rexsng |
|- ( A e. X -> ( E. i e. { A } K e. ( { <. A , { N } >. } ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) ) |
22 |
2 21
|
syl |
|- ( ph -> ( E. i e. { A } K e. ( { <. A , { N } >. } ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) ) |
23 |
18 22
|
bitrd |
|- ( ph -> ( E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) <-> K e. ( { <. A , { N } >. } ` A ) ) ) |
24 |
11 23
|
mtbird |
|- ( ph -> -. E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) ) |
25 |
5
|
eldifad |
|- ( ph -> K e. V ) |
26 |
1
|
eleq2d |
|- ( ph -> ( K e. ( Vtx ` G ) <-> K e. V ) ) |
27 |
25 26
|
mpbird |
|- ( ph -> K e. ( Vtx ` G ) ) |
28 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
29 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
30 |
|
eqid |
|- ( VtxDeg ` G ) = ( VtxDeg ` G ) |
31 |
28 29 30
|
vtxd0nedgb |
|- ( K e. ( Vtx ` G ) -> ( ( ( VtxDeg ` G ) ` K ) = 0 <-> -. E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) ) ) |
32 |
27 31
|
syl |
|- ( ph -> ( ( ( VtxDeg ` G ) ` K ) = 0 <-> -. E. i e. dom ( iEdg ` G ) K e. ( ( iEdg ` G ) ` i ) ) ) |
33 |
24 32
|
mpbird |
|- ( ph -> ( ( VtxDeg ` G ) ` K ) = 0 ) |