Step |
Hyp |
Ref |
Expression |
1 |
|
eqid |
|- ( Vtx ` G ) = ( Vtx ` G ) |
2 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
3 |
1 2
|
uhgrf |
|- ( G e. UHGraph -> ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) ) |
4 |
|
pweq |
|- ( ( Vtx ` G ) = (/) -> ~P ( Vtx ` G ) = ~P (/) ) |
5 |
4
|
difeq1d |
|- ( ( Vtx ` G ) = (/) -> ( ~P ( Vtx ` G ) \ { (/) } ) = ( ~P (/) \ { (/) } ) ) |
6 |
|
pw0 |
|- ~P (/) = { (/) } |
7 |
6
|
difeq1i |
|- ( ~P (/) \ { (/) } ) = ( { (/) } \ { (/) } ) |
8 |
|
difid |
|- ( { (/) } \ { (/) } ) = (/) |
9 |
7 8
|
eqtri |
|- ( ~P (/) \ { (/) } ) = (/) |
10 |
5 9
|
eqtrdi |
|- ( ( Vtx ` G ) = (/) -> ( ~P ( Vtx ` G ) \ { (/) } ) = (/) ) |
11 |
10
|
adantl |
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ~P ( Vtx ` G ) \ { (/) } ) = (/) ) |
12 |
11
|
feq3d |
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) <-> ( iEdg ` G ) : dom ( iEdg ` G ) --> (/) ) ) |
13 |
|
f00 |
|- ( ( iEdg ` G ) : dom ( iEdg ` G ) --> (/) <-> ( ( iEdg ` G ) = (/) /\ dom ( iEdg ` G ) = (/) ) ) |
14 |
13
|
simplbi |
|- ( ( iEdg ` G ) : dom ( iEdg ` G ) --> (/) -> ( iEdg ` G ) = (/) ) |
15 |
12 14
|
syl6bi |
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ( iEdg ` G ) : dom ( iEdg ` G ) --> ( ~P ( Vtx ` G ) \ { (/) } ) -> ( iEdg ` G ) = (/) ) ) |
16 |
3 15
|
syl5 |
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph -> ( iEdg ` G ) = (/) ) ) |
17 |
|
simpl |
|- ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> G e. W ) |
18 |
|
simpr |
|- ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> ( iEdg ` G ) = (/) ) |
19 |
17 18
|
uhgr0e |
|- ( ( G e. W /\ ( iEdg ` G ) = (/) ) -> G e. UHGraph ) |
20 |
19
|
ex |
|- ( G e. W -> ( ( iEdg ` G ) = (/) -> G e. UHGraph ) ) |
21 |
20
|
adantr |
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( ( iEdg ` G ) = (/) -> G e. UHGraph ) ) |
22 |
16 21
|
impbid |
|- ( ( G e. W /\ ( Vtx ` G ) = (/) ) -> ( G e. UHGraph <-> ( iEdg ` G ) = (/) ) ) |