Step |
Hyp |
Ref |
Expression |
1 |
|
1hevtxdg0.i |
|- ( ph -> ( iEdg ` G ) = { <. A , E >. } ) |
2 |
|
1hevtxdg0.v |
|- ( ph -> ( Vtx ` G ) = V ) |
3 |
|
1hevtxdg0.a |
|- ( ph -> A e. X ) |
4 |
|
1hevtxdg0.d |
|- ( ph -> D e. V ) |
5 |
|
1hevtxdg0.e |
|- ( ph -> E e. Y ) |
6 |
|
1hevtxdg0.n |
|- ( ph -> D e/ E ) |
7 |
|
df-nel |
|- ( D e/ E <-> -. D e. E ) |
8 |
6 7
|
sylib |
|- ( ph -> -. D e. E ) |
9 |
1
|
fveq1d |
|- ( ph -> ( ( iEdg ` G ) ` A ) = ( { <. A , E >. } ` A ) ) |
10 |
|
fvsng |
|- ( ( A e. X /\ E e. Y ) -> ( { <. A , E >. } ` A ) = E ) |
11 |
3 5 10
|
syl2anc |
|- ( ph -> ( { <. A , E >. } ` A ) = E ) |
12 |
9 11
|
eqtrd |
|- ( ph -> ( ( iEdg ` G ) ` A ) = E ) |
13 |
8 12
|
neleqtrrd |
|- ( ph -> -. D e. ( ( iEdg ` G ) ` A ) ) |
14 |
|
fveq2 |
|- ( x = A -> ( ( iEdg ` G ) ` x ) = ( ( iEdg ` G ) ` A ) ) |
15 |
14
|
eleq2d |
|- ( x = A -> ( D e. ( ( iEdg ` G ) ` x ) <-> D e. ( ( iEdg ` G ) ` A ) ) ) |
16 |
15
|
notbid |
|- ( x = A -> ( -. D e. ( ( iEdg ` G ) ` x ) <-> -. D e. ( ( iEdg ` G ) ` A ) ) ) |
17 |
16
|
ralsng |
|- ( A e. X -> ( A. x e. { A } -. D e. ( ( iEdg ` G ) ` x ) <-> -. D e. ( ( iEdg ` G ) ` A ) ) ) |
18 |
3 17
|
syl |
|- ( ph -> ( A. x e. { A } -. D e. ( ( iEdg ` G ) ` x ) <-> -. D e. ( ( iEdg ` G ) ` A ) ) ) |
19 |
13 18
|
mpbird |
|- ( ph -> A. x e. { A } -. D e. ( ( iEdg ` G ) ` x ) ) |
20 |
1
|
dmeqd |
|- ( ph -> dom ( iEdg ` G ) = dom { <. A , E >. } ) |
21 |
|
dmsnopg |
|- ( E e. Y -> dom { <. A , E >. } = { A } ) |
22 |
5 21
|
syl |
|- ( ph -> dom { <. A , E >. } = { A } ) |
23 |
20 22
|
eqtrd |
|- ( ph -> dom ( iEdg ` G ) = { A } ) |
24 |
23
|
raleqdv |
|- ( ph -> ( A. x e. dom ( iEdg ` G ) -. D e. ( ( iEdg ` G ) ` x ) <-> A. x e. { A } -. D e. ( ( iEdg ` G ) ` x ) ) ) |
25 |
19 24
|
mpbird |
|- ( ph -> A. x e. dom ( iEdg ` G ) -. D e. ( ( iEdg ` G ) ` x ) ) |
26 |
|
ralnex |
|- ( A. x e. dom ( iEdg ` G ) -. D e. ( ( iEdg ` G ) ` x ) <-> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) ) |
27 |
25 26
|
sylib |
|- ( ph -> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) ) |
28 |
2
|
eleq2d |
|- ( ph -> ( D e. ( Vtx ` G ) <-> D e. V ) ) |
29 |
4 28
|
mpbird |
|- ( ph -> D e. ( Vtx ` G ) ) |
30 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
31 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
32 |
|
eqid |
|- ( VtxDeg ` G ) = ( VtxDeg ` G ) |
33 |
30 31 32
|
vtxd0nedgb |
|- ( D e. ( Vtx ` G ) -> ( ( ( VtxDeg ` G ) ` D ) = 0 <-> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) ) ) |
34 |
29 33
|
syl |
|- ( ph -> ( ( ( VtxDeg ` G ) ` D ) = 0 <-> -. E. x e. dom ( iEdg ` G ) D e. ( ( iEdg ` G ) ` x ) ) ) |
35 |
27 34
|
mpbird |
|- ( ph -> ( ( VtxDeg ` G ) ` D ) = 0 ) |