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 )