Step |
Hyp |
Ref |
Expression |
1 |
|
vtxdushgrfvedg.v |
|- V = ( Vtx ` G ) |
2 |
|
vtxdushgrfvedg.e |
|- E = ( Edg ` G ) |
3 |
|
fvex |
|- ( iEdg ` G ) e. _V |
4 |
3
|
dmex |
|- dom ( iEdg ` G ) e. _V |
5 |
4
|
rabex |
|- { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } e. _V |
6 |
5
|
a1i |
|- ( ( G e. USHGraph /\ U e. V ) -> { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } e. _V ) |
7 |
|
eqid |
|- ( iEdg ` G ) = ( iEdg ` G ) |
8 |
|
eqid |
|- { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } = { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } |
9 |
|
eleq2w |
|- ( e = c -> ( U e. e <-> U e. c ) ) |
10 |
9
|
cbvrabv |
|- { e e. E | U e. e } = { c e. E | U e. c } |
11 |
|
eqid |
|- ( x e. { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } |-> ( ( iEdg ` G ) ` x ) ) = ( x e. { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } |-> ( ( iEdg ` G ) ` x ) ) |
12 |
2 7 1 8 10 11
|
ushgredgedg |
|- ( ( G e. USHGraph /\ U e. V ) -> ( x e. { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } |-> ( ( iEdg ` G ) ` x ) ) : { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } -1-1-onto-> { e e. E | U e. e } ) |
13 |
6 12
|
hasheqf1od |
|- ( ( G e. USHGraph /\ U e. V ) -> ( # ` { i e. dom ( iEdg ` G ) | U e. ( ( iEdg ` G ) ` i ) } ) = ( # ` { e e. E | U e. e } ) ) |