Theorem structvtxval

Description: The set of vertices of an extensible structure with a base set and another slot. (Contributed by AV, 23-Sep-2020) (Proof shortened by AV, 12-Nov-2021)

	Ref	Expression
Hypotheses	structvtxvallem.s	$$⊢S\in \mathbb{N}$$
	structvtxvallem.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<S$$
	structvtxvallem.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}$$
Assertion	structvtxval	$$⊢\left(V\in X\wedge E\in Y\right)\to \mathrm{Vtx}\left(G\right)=V$$

Proof

Step	Hyp	Ref	Expression
1		structvtxvallem.s	$$⊢S\in \mathbb{N}$$
2		structvtxvallem.b	$$⊢{\mathrm{Base}}_{\mathrm{ndx}}<S$$
3		structvtxvallem.g	$$⊢G=\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}$$
4	3 2 1	2strstr	$$⊢G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},S⟩$$
5	4	a1i	$$⊢\left(V\in X\wedge E\in Y\right)\to G\mathrm{Struct}⟨{\mathrm{Base}}_{\mathrm{ndx}},S⟩$$
6	1 2 3	structvtxvallem	$$⊢\left(V\in X\wedge E\in Y\right)\to 2\le \left|\mathrm{dom}G\right|$$
7		simpl	$$⊢\left(V\in X\wedge E\in Y\right)\to V\in X$$
8		opex	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in \mathrm{V}$$
9	8	prid1	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨S,E⟩\right\}$$
10	9 3	eleqtrri	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in G$$
11	10	a1i	$$⊢\left(V\in X\wedge E\in Y\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in G$$
12	5 6 7 11	basvtxval	$$⊢\left(V\in X\wedge E\in Y\right)\to \mathrm{Vtx}\left(G\right)=V$$