Theorem setsvtx

Description: The vertices of a structure with a base set and an inserted resp. replaced slot for the edge function. (Contributed by AV, 18-Jan-2020) (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	setsvtx	$$⊢\phi \to \mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)={\mathrm{Base}}_G$$

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	1	fvexi	$$⊢I\in \mathrm{V}$$
6	5	a1i	$$⊢\phi \to I\in \mathrm{V}$$
7	2 6 4	setsn0fun	$$⊢\phi \to \mathrm{Fun}\left(\left(G\mathrm{sSet}⟨I,E⟩\right)\setminus \left\{\varnothing \right\}\right)$$
8	1	eqcomi	$$⊢\mathrm{ef}\left(\mathrm{ndx}\right)=I$$
9	8	preq2i	$$⊢\left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}=\left\{{\mathrm{Base}}_{\mathrm{ndx}},I\right\}$$
10	2 6 4 3	basprssdmsets	$$⊢\phi \to \left\{{\mathrm{Base}}_{\mathrm{ndx}},I\right\}\subseteq \mathrm{dom}\left(G\mathrm{sSet}⟨I,E⟩\right)$$
11	9 10	eqsstrid	$$⊢\phi \to \left\{{\mathrm{Base}}_{\mathrm{ndx}},\mathrm{ef}\left(\mathrm{ndx}\right)\right\}\subseteq \mathrm{dom}\left(G\mathrm{sSet}⟨I,E⟩\right)$$
12		funvtxval	$$⊢\left(\mathrm{Fun}\left(\left(G\mathrm{sSet}⟨I,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}⟨I,E⟩\right)\right)\to \mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)={\mathrm{Base}}_{\left(G\mathrm{sSet}⟨I,E⟩\right)}$$
13	7 11 12	syl2anc	$$⊢\phi \to \mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)={\mathrm{Base}}_{\left(G\mathrm{sSet}⟨I,E⟩\right)}$$
14		baseid	$$⊢\mathrm{Base}=\mathrm{Slot}{\mathrm{Base}}_{\mathrm{ndx}}$$
15		basendxnedgfndx	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne \mathrm{ef}\left(\mathrm{ndx}\right)$$
16	15 1	neeqtrri	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\ne I$$
17	14 16	setsnid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_{\left(G\mathrm{sSet}⟨I,E⟩\right)}$$
18	13 17	eqtr4di	$$⊢\phi \to \mathrm{Vtx}\left(G\mathrm{sSet}⟨I,E⟩\right)={\mathrm{Base}}_G$$