# 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}=\mathrm{ef}\left(\mathrm{ndx}\right)$
setsvtx.s ${⊢}{\phi }\to {G}\mathrm{Struct}{X}$
setsvtx.b ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}{G}$
setsvtx.e ${⊢}{\phi }\to {E}\in {W}$
Assertion setsiedg ${⊢}{\phi }\to \mathrm{iEdg}\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)={E}$

### Proof

Step Hyp Ref Expression
1 setsvtx.i ${⊢}{I}=\mathrm{ef}\left(\mathrm{ndx}\right)$
2 setsvtx.s ${⊢}{\phi }\to {G}\mathrm{Struct}{X}$
3 setsvtx.b ${⊢}{\phi }\to {\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{dom}{G}$
4 setsvtx.e ${⊢}{\phi }\to {E}\in {W}$
5 fvexd ${⊢}{\phi }\to \mathrm{ef}\left(\mathrm{ndx}\right)\in \mathrm{V}$
6 2 5 4 setsn0fun ${⊢}{\phi }\to \mathrm{Fun}\left(\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)\setminus \left\{\varnothing \right\}\right)$
7 2 5 4 3 basprssdmsets ${⊢}{\phi }\to \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}\subseteq \mathrm{dom}\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)$
8 funiedgval ${⊢}\left(\mathrm{Fun}\left(\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)\setminus \left\{\varnothing \right\}\right)\wedge \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}\subseteq \mathrm{dom}\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)\right)\to \mathrm{iEdg}\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)=\mathrm{ef}\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)$
9 6 7 8 syl2anc ${⊢}{\phi }\to \mathrm{iEdg}\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)=\mathrm{ef}\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)$
10 1 opeq1i ${⊢}⟨{I},{E}⟩=⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩$
11 10 oveq2i ${⊢}{G}\mathrm{sSet}⟨{I},{E}⟩={G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩$
12 11 fveq2i ${⊢}\mathrm{iEdg}\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)=\mathrm{iEdg}\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)$
13 12 a1i ${⊢}{\phi }\to \mathrm{iEdg}\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)=\mathrm{iEdg}\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)$
14 structex ${⊢}{G}\mathrm{Struct}{X}\to {G}\in \mathrm{V}$
15 2 14 syl ${⊢}{\phi }\to {G}\in \mathrm{V}$
16 edgfid ${⊢}\mathrm{ef}=\mathrm{Slot}\mathrm{ef}\left(\mathrm{ndx}\right)$
17 16 setsid ${⊢}\left({G}\in \mathrm{V}\wedge {E}\in {W}\right)\to {E}=\mathrm{ef}\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)$
18 15 4 17 syl2anc ${⊢}{\phi }\to {E}=\mathrm{ef}\left({G}\mathrm{sSet}⟨\mathrm{ef}\left(\mathrm{ndx}\right),{E}⟩\right)$
19 9 13 18 3eqtr4d ${⊢}{\phi }\to \mathrm{iEdg}\left({G}\mathrm{sSet}⟨{I},{E}⟩\right)={E}$