Step |
Hyp |
Ref |
Expression |
1 |
|
setsvtx.i |
|- I = ( .ef ` ndx ) |
2 |
|
setsvtx.s |
|- ( ph -> G Struct X ) |
3 |
|
setsvtx.b |
|- ( ph -> ( Base ` ndx ) e. dom G ) |
4 |
|
setsvtx.e |
|- ( ph -> E e. W ) |
5 |
|
fvexd |
|- ( ph -> ( .ef ` ndx ) e. _V ) |
6 |
2 5 4
|
setsn0fun |
|- ( ph -> Fun ( ( G sSet <. ( .ef ` ndx ) , E >. ) \ { (/) } ) ) |
7 |
2 5 4 3
|
basprssdmsets |
|- ( ph -> { ( Base ` ndx ) , ( .ef ` ndx ) } C_ dom ( G sSet <. ( .ef ` ndx ) , E >. ) ) |
8 |
|
funiedgval |
|- ( ( Fun ( ( G sSet <. ( .ef ` ndx ) , E >. ) \ { (/) } ) /\ { ( Base ` ndx ) , ( .ef ` ndx ) } C_ dom ( G sSet <. ( .ef ` ndx ) , E >. ) ) -> ( iEdg ` ( G sSet <. ( .ef ` ndx ) , E >. ) ) = ( .ef ` ( G sSet <. ( .ef ` ndx ) , E >. ) ) ) |
9 |
6 7 8
|
syl2anc |
|- ( ph -> ( iEdg ` ( G sSet <. ( .ef ` ndx ) , E >. ) ) = ( .ef ` ( G sSet <. ( .ef ` ndx ) , E >. ) ) ) |
10 |
1
|
opeq1i |
|- <. I , E >. = <. ( .ef ` ndx ) , E >. |
11 |
10
|
oveq2i |
|- ( G sSet <. I , E >. ) = ( G sSet <. ( .ef ` ndx ) , E >. ) |
12 |
11
|
fveq2i |
|- ( iEdg ` ( G sSet <. I , E >. ) ) = ( iEdg ` ( G sSet <. ( .ef ` ndx ) , E >. ) ) |
13 |
12
|
a1i |
|- ( ph -> ( iEdg ` ( G sSet <. I , E >. ) ) = ( iEdg ` ( G sSet <. ( .ef ` ndx ) , E >. ) ) ) |
14 |
|
structex |
|- ( G Struct X -> G e. _V ) |
15 |
2 14
|
syl |
|- ( ph -> G e. _V ) |
16 |
|
edgfid |
|- .ef = Slot ( .ef ` ndx ) |
17 |
16
|
setsid |
|- ( ( G e. _V /\ E e. W ) -> E = ( .ef ` ( G sSet <. ( .ef ` ndx ) , E >. ) ) ) |
18 |
15 4 17
|
syl2anc |
|- ( ph -> E = ( .ef ` ( G sSet <. ( .ef ` ndx ) , E >. ) ) ) |
19 |
9 13 18
|
3eqtr4d |
|- ( ph -> ( iEdg ` ( G sSet <. I , E >. ) ) = E ) |