Step |
Hyp |
Ref |
Expression |
1 |
|
usgr1v |
|- ( ( G e. W /\ ( Vtx ` G ) = { A } ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) ) |
2 |
1
|
3adant3 |
|- ( ( G e. W /\ ( Vtx ` G ) = { A } /\ Fun ( iEdg ` G ) ) -> ( G e. USGraph <-> ( iEdg ` G ) = (/) ) ) |
3 |
|
funrel |
|- ( Fun ( iEdg ` G ) -> Rel ( iEdg ` G ) ) |
4 |
|
relrn0 |
|- ( Rel ( iEdg ` G ) -> ( ( iEdg ` G ) = (/) <-> ran ( iEdg ` G ) = (/) ) ) |
5 |
3 4
|
syl |
|- ( Fun ( iEdg ` G ) -> ( ( iEdg ` G ) = (/) <-> ran ( iEdg ` G ) = (/) ) ) |
6 |
5
|
3ad2ant3 |
|- ( ( G e. W /\ ( Vtx ` G ) = { A } /\ Fun ( iEdg ` G ) ) -> ( ( iEdg ` G ) = (/) <-> ran ( iEdg ` G ) = (/) ) ) |
7 |
|
edgval |
|- ( Edg ` G ) = ran ( iEdg ` G ) |
8 |
7
|
eqcomi |
|- ran ( iEdg ` G ) = ( Edg ` G ) |
9 |
8
|
eqeq1i |
|- ( ran ( iEdg ` G ) = (/) <-> ( Edg ` G ) = (/) ) |
10 |
9
|
a1i |
|- ( ( G e. W /\ ( Vtx ` G ) = { A } /\ Fun ( iEdg ` G ) ) -> ( ran ( iEdg ` G ) = (/) <-> ( Edg ` G ) = (/) ) ) |
11 |
2 6 10
|
3bitrd |
|- ( ( G e. W /\ ( Vtx ` G ) = { A } /\ Fun ( iEdg ` G ) ) -> ( G e. USGraph <-> ( Edg ` G ) = (/) ) ) |