Step |
Hyp |
Ref |
Expression |
1 |
|
edgval |
|- ( Edg ` G ) = ran ( iEdg ` G ) |
2 |
1
|
a1i |
|- ( G e. W -> ( Edg ` G ) = ran ( iEdg ` G ) ) |
3 |
2
|
eqeq1d |
|- ( G e. W -> ( ( Edg ` G ) = (/) <-> ran ( iEdg ` G ) = (/) ) ) |
4 |
|
funrel |
|- ( Fun ( iEdg ` G ) -> Rel ( iEdg ` G ) ) |
5 |
|
relrn0 |
|- ( Rel ( iEdg ` G ) -> ( ( iEdg ` G ) = (/) <-> ran ( iEdg ` G ) = (/) ) ) |
6 |
5
|
bicomd |
|- ( Rel ( iEdg ` G ) -> ( ran ( iEdg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) ) |
7 |
4 6
|
syl |
|- ( Fun ( iEdg ` G ) -> ( ran ( iEdg ` G ) = (/) <-> ( iEdg ` G ) = (/) ) ) |
8 |
|
simpr |
|- ( ( ( iEdg ` G ) = (/) /\ G e. W ) -> G e. W ) |
9 |
|
simpl |
|- ( ( ( iEdg ` G ) = (/) /\ G e. W ) -> ( iEdg ` G ) = (/) ) |
10 |
8 9
|
usgr0e |
|- ( ( ( iEdg ` G ) = (/) /\ G e. W ) -> G e. USGraph ) |
11 |
10
|
ex |
|- ( ( iEdg ` G ) = (/) -> ( G e. W -> G e. USGraph ) ) |
12 |
7 11
|
syl6bi |
|- ( Fun ( iEdg ` G ) -> ( ran ( iEdg ` G ) = (/) -> ( G e. W -> G e. USGraph ) ) ) |
13 |
12
|
com13 |
|- ( G e. W -> ( ran ( iEdg ` G ) = (/) -> ( Fun ( iEdg ` G ) -> G e. USGraph ) ) ) |
14 |
3 13
|
sylbid |
|- ( G e. W -> ( ( Edg ` G ) = (/) -> ( Fun ( iEdg ` G ) -> G e. USGraph ) ) ) |
15 |
14
|
3imp |
|- ( ( G e. W /\ ( Edg ` G ) = (/) /\ Fun ( iEdg ` G ) ) -> G e. USGraph ) |