This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )