Theorem structgrssvtx

Description: The set of vertices of a graph represented as an extensible structure with vertices as base set and indexed edges. (Contributed by AV, 14-Oct-2020) (Proof shortened by AV, 12-Nov-2021)

	Ref	Expression
Hypotheses	structgrssvtx.g	$$⊢\phi \to G\mathrm{Struct}X$$
	structgrssvtx.v	$$⊢\phi \to V\in Y$$
	structgrssvtx.e	$$⊢\phi \to E\in Z$$
	structgrssvtx.s	$$⊢\phi \to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\right\}\subseteq G$$
Assertion	structgrssvtx	$$⊢\phi \to \mathrm{Vtx}\left(G\right)=V$$

Proof

Step	Hyp	Ref	Expression
1		structgrssvtx.g	$$⊢\phi \to G\mathrm{Struct}X$$
2		structgrssvtx.v	$$⊢\phi \to V\in Y$$
3		structgrssvtx.e	$$⊢\phi \to E\in Z$$
4		structgrssvtx.s	$$⊢\phi \to \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\right\}\subseteq G$$
5	1 2 3 4	structgrssvtxlem	$$⊢\phi \to 2\le \left|\mathrm{dom}G\right|$$
6		opex	$$⊢⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in \mathrm{V}$$
7		opex	$$⊢⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\in \mathrm{V}$$
8	6 7	prss	$$⊢\left(⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in G\wedge ⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\in G\right)\leftrightarrow \left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\right\}\subseteq G$$
9		simpl	$$⊢\left(⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in G\wedge ⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\in G\right)\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in G$$
10	8 9	sylbir	$$⊢\left\{⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩,⟨\mathrm{ef}\left(\mathrm{ndx}\right),E⟩\right\}\subseteq G\to ⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in G$$
11	4 10	syl	$$⊢\phi \to ⟨{\mathrm{Base}}_{\mathrm{ndx}},V⟩\in G$$
12	1 5 2 11	basvtxval	$$⊢\phi \to \mathrm{Vtx}\left(G\right)=V$$