Step |
Hyp |
Ref |
Expression |
1 |
|
basvtxval.s |
|- ( ph -> G Struct X ) |
2 |
|
basvtxval.d |
|- ( ph -> 2 <_ ( # ` dom G ) ) |
3 |
|
edgfiedgval.e |
|- ( ph -> E e. Y ) |
4 |
|
edgfiedgval.f |
|- ( ph -> <. ( .ef ` ndx ) , E >. e. G ) |
5 |
|
structn0fun |
|- ( G Struct X -> Fun ( G \ { (/) } ) ) |
6 |
1 5
|
syl |
|- ( ph -> Fun ( G \ { (/) } ) ) |
7 |
|
funiedgdmge2val |
|- ( ( Fun ( G \ { (/) } ) /\ 2 <_ ( # ` dom G ) ) -> ( iEdg ` G ) = ( .ef ` G ) ) |
8 |
6 2 7
|
syl2anc |
|- ( ph -> ( iEdg ` G ) = ( .ef ` G ) ) |
9 |
|
edgfid |
|- .ef = Slot ( .ef ` ndx ) |
10 |
|
structex |
|- ( G Struct X -> G e. _V ) |
11 |
1 10
|
syl |
|- ( ph -> G e. _V ) |
12 |
|
structfung |
|- ( G Struct X -> Fun `' `' G ) |
13 |
1 12
|
syl |
|- ( ph -> Fun `' `' G ) |
14 |
9 11 13 4 3
|
strfv2d |
|- ( ph -> E = ( .ef ` G ) ) |
15 |
8 14
|
eqtr4d |
|- ( ph -> ( iEdg ` G ) = E ) |