Theorem umgr2v2evtx

Description: The set of vertices in a multigraph with two edges connecting the same two vertices. (Contributed by AV, 17-Dec-2020)

	Ref	Expression
Hypothesis	umgr2v2evtx.g	$$⊢G=⟨V,\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}⟩$$
Assertion	umgr2v2evtx	$$⊢V\in W\to \mathrm{Vtx}\left(G\right)=V$$

Proof

Step	Hyp	Ref	Expression
1		umgr2v2evtx.g	$$⊢G=⟨V,\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}⟩$$
2	1	fveq2i	$$⊢\mathrm{Vtx}\left(G\right)=\mathrm{Vtx}\left(⟨V,\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}⟩\right)$$
3		prex	$$⊢\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}\in \mathrm{V}$$
4		opvtxfv	$$⊢\left(V\in W\wedge \left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}\in \mathrm{V}\right)\to \mathrm{Vtx}\left(⟨V,\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}⟩\right)=V$$
5	3 4	mpan2	$$⊢V\in W\to \mathrm{Vtx}\left(⟨V,\left\{⟨0,\left\{A,B\right\}⟩,⟨1,\left\{A,B\right\}⟩\right\}⟩\right)=V$$
6	2 5	syl5eq	$$⊢V\in W\to \mathrm{Vtx}\left(G\right)=V$$