Theorem usgrexmplvtx

Description: The vertices 0 , 1 , 2 , 3 , 4 of the graph G = <. V , E >. . (Contributed by AV, 12-Jan-2020) (Revised by AV, 21-Oct-2020)

	Ref	Expression
Hypotheses	usgrexmpl.v	$$⊢V=\left(0\dots 4\right)$$
	usgrexmpl.e	$$⊢E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,0\right\}\left\{0,3\right\}”⟩$$
	usgrexmpl.g	$$⊢G=⟨V,E⟩$$
Assertion	usgrexmplvtx	$$⊢\mathrm{Vtx}\left(G\right)=\left\{0,1,2\right\}\cup \left\{3,4\right\}$$

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl.v	$$⊢V=\left(0\dots 4\right)$$
2		usgrexmpl.e	$$⊢E=⟨“\left\{0,1\right\}\left\{1,2\right\}\left\{2,0\right\}\left\{0,3\right\}”⟩$$
3		usgrexmpl.g	$$⊢G=⟨V,E⟩$$
4	1 2 3	usgrexmpllem	$$⊢\left(\mathrm{Vtx}\left(G\right)=V\wedge \mathrm{iEdg}\left(G\right)=E\right)$$
5		id	$$⊢\mathrm{Vtx}\left(G\right)=V\to \mathrm{Vtx}\left(G\right)=V$$
6		fz0to4untppr	$$⊢\left(0\dots 4\right)=\left\{0,1,2\right\}\cup \left\{3,4\right\}$$
7	1 6	eqtri	$$⊢V=\left\{0,1,2\right\}\cup \left\{3,4\right\}$$
8	5 7	syl6eq	$$⊢\mathrm{Vtx}\left(G\right)=V\to \mathrm{Vtx}\left(G\right)=\left\{0,1,2\right\}\cup \left\{3,4\right\}$$
9	8	adantr	$$⊢\left(\mathrm{Vtx}\left(G\right)=V\wedge \mathrm{iEdg}\left(G\right)=E\right)\to \mathrm{Vtx}\left(G\right)=\left\{0,1,2\right\}\cup \left\{3,4\right\}$$
10	4 9	ax-mp	$$⊢\mathrm{Vtx}\left(G\right)=\left\{0,1,2\right\}\cup \left\{3,4\right\}$$