Theorem usgrexmpl1vtx

Description: The vertices 0 , 1 , 2 , 3 , 4 , 5 of the graph G = <. V , E >. . (Contributed by AV, 3-Aug-2025)

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

Proof

Step	Hyp	Ref	Expression
1		usgrexmpl1.v	$$⊢V=\left(0\dots 5\right)$$
2		usgrexmpl1.e	$$⊢E=⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{1,2\right\}\left\{0,3\right\}\left\{3,4\right\}\left\{3,5\right\}\left\{4,5\right\}”⟩$$
3		usgrexmpl1.g	$$⊢G=⟨V,E⟩$$
4	3	fveq2i	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(⟨V,E⟩\right)$$
5	1	ovexi	$$⊢V\in \mathrm{V}$$
6		s7cli	$$⊢⟨“\left\{0,1\right\}\left\{0,2\right\}\left\{1,2\right\}\left\{0,3\right\}\left\{3,4\right\}\left\{3,5\right\}\left\{4,5\right\}”⟩\in \mathrm{Word}\mathrm{V}$$
7	2 6	eqeltri	$$⊢E\in \mathrm{Word}\mathrm{V}$$
8		opvtxfv	$$⊢\left(V\in \mathrm{V}\wedge E\in \mathrm{Word}\mathrm{V}\right)\to \mathrm{Vtx}\left(⟨V,E⟩\right)=V$$
9	5 7 8	mp2an	$$⊢\mathrm{Vtx}\left(⟨V,E⟩\right)=V$$
10	4 9	eqtri	$$⊢\mathrm{Vtx}\left(G\right)=V$$
11		fz0to5un2tp	$$⊢\left(0\dots 5\right)=\left\{0,1,2\right\}\cup \left\{3,4,5\right\}$$
12	10 1 11	3eqtri	$$⊢\mathrm{Vtx}\left(G\right)=\left\{0,1,2\right\}\cup \left\{3,4,5\right\}$$