Step |
Hyp |
Ref |
Expression |
1 |
|
opex |
|- <. V , E >. e. _V |
2 |
|
eqid |
|- ( Vtx ` <. V , E >. ) = ( Vtx ` <. V , E >. ) |
3 |
|
eqid |
|- ( iEdg ` <. V , E >. ) = ( iEdg ` <. V , E >. ) |
4 |
2 3
|
isuhgr |
|- ( <. V , E >. e. _V -> ( <. V , E >. e. UHGraph <-> ( iEdg ` <. V , E >. ) : dom ( iEdg ` <. V , E >. ) --> ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) ) ) |
5 |
1 4
|
mp1i |
|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. UHGraph <-> ( iEdg ` <. V , E >. ) : dom ( iEdg ` <. V , E >. ) --> ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) ) ) |
6 |
|
opiedgfv |
|- ( ( V e. W /\ E e. X ) -> ( iEdg ` <. V , E >. ) = E ) |
7 |
6
|
dmeqd |
|- ( ( V e. W /\ E e. X ) -> dom ( iEdg ` <. V , E >. ) = dom E ) |
8 |
|
opvtxfv |
|- ( ( V e. W /\ E e. X ) -> ( Vtx ` <. V , E >. ) = V ) |
9 |
8
|
pweqd |
|- ( ( V e. W /\ E e. X ) -> ~P ( Vtx ` <. V , E >. ) = ~P V ) |
10 |
9
|
difeq1d |
|- ( ( V e. W /\ E e. X ) -> ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) = ( ~P V \ { (/) } ) ) |
11 |
6 7 10
|
feq123d |
|- ( ( V e. W /\ E e. X ) -> ( ( iEdg ` <. V , E >. ) : dom ( iEdg ` <. V , E >. ) --> ( ~P ( Vtx ` <. V , E >. ) \ { (/) } ) <-> E : dom E --> ( ~P V \ { (/) } ) ) ) |
12 |
5 11
|
bitrd |
|- ( ( V e. W /\ E e. X ) -> ( <. V , E >. e. UHGraph <-> E : dom E --> ( ~P V \ { (/) } ) ) ) |