Metamath Proof Explorer


Theorem setsiedg

Description: The (indexed) edges of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 7-Jun-2021) (Revised by AV, 16-Nov-2021)

Ref Expression
Hypotheses setsvtx.i
|- I = ( .ef ` ndx )
setsvtx.s
|- ( ph -> G Struct X )
setsvtx.b
|- ( ph -> ( Base ` ndx ) e. dom G )
setsvtx.e
|- ( ph -> E e. W )
Assertion setsiedg
|- ( ph -> ( iEdg ` ( G sSet <. I , E >. ) ) = E )

Proof

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 )