Theorem funvtxdm2val

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

	Ref	Expression
Hypotheses	funvtxdm2val.a	$$⊢A\in \mathrm{V}$$
	funvtxdm2val.b	$$⊢B\in \mathrm{V}$$
Assertion	funvtxdm2val	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge A\ne B\wedge \left\{A,B\right\}\subseteq \mathrm{dom}G\right)\to \mathrm{Vtx}\left(G\right)={\mathrm{Base}}_G$$

Proof

Step	Hyp	Ref	Expression
1		funvtxdm2val.a	$$⊢A\in \mathrm{V}$$
2		funvtxdm2val.b	$$⊢B\in \mathrm{V}$$
3		vtxval	$$⊢\mathrm{Vtx}\left(G\right)=if\left(G\in \left(\mathrm{V}\times \mathrm{V}\right),1^{st}\left(G\right),{\mathrm{Base}}_G\right)$$
4	1 2	fun2dmnop0	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge A\ne B\wedge \left\{A,B\right\}\subseteq \mathrm{dom}G\right)\to \neg G\in \left(\mathrm{V}\times \mathrm{V}\right)$$
5	4	iffalsed	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge A\ne B\wedge \left\{A,B\right\}\subseteq \mathrm{dom}G\right)\to if\left(G\in \left(\mathrm{V}\times \mathrm{V}\right),1^{st}\left(G\right),{\mathrm{Base}}_G\right)={\mathrm{Base}}_G$$
6	3 5	eqtrid	$$⊢\left(\mathrm{Fun}\left(G\setminus \left\{\varnothing \right\}\right)\wedge A\ne B\wedge \left\{A,B\right\}\subseteq \mathrm{dom}G\right)\to \mathrm{Vtx}\left(G\right)={\mathrm{Base}}_G$$