Theorem funvtxval0

Description: The set of vertices of an extensible structure with a base set and (at least) another slot. (Contributed by AV, 22-Sep-2020) (Revised by AV, 7-Jun-2021) (Revised by AV, 12-Nov-2021)

	Ref	Expression
Hypothesis	funvtxval0.s	$$⊢S\in \mathrm{V}$$
Assertion	funvtxval0	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge S\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge \left\{{\mathrm{Base}}_{\mathrm{ndx}},S\right\}\subseteq \mathrm{dom}G\right)\to \mathrm{Vtx}\left(G\right)={\mathrm{Base}}_G$$

Proof

Step	Hyp	Ref	Expression
1		funvtxval0.s	$$⊢S\in \mathrm{V}$$
2		necom	$$⊢S\ne {\mathrm{Base}}_{\mathrm{ndx}}\leftrightarrow {\mathrm{Base}}_{\mathrm{ndx}}\ne S$$
3		fvex	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}\in \mathrm{V}$$
4	3 1	funvtxdm2val	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge {\mathrm{Base}}_{\mathrm{ndx}}\ne S\wedge \left\{{\mathrm{Base}}_{\mathrm{ndx}},S\right\}\subseteq \mathrm{dom}G\right)\to \mathrm{Vtx}\left(G\right)={\mathrm{Base}}_G$$
5	2 4	syl3an2b	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge S\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge \left\{{\mathrm{Base}}_{\mathrm{ndx}},S\right\}\subseteq \mathrm{dom}G\right)\to \mathrm{Vtx}\left(G\right)={\mathrm{Base}}_G$$