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	⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
Assertion	umgr2v2evtx	⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 )

Proof

Step	Hyp	Ref	Expression
1		umgr2v2evtx.g	⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩
2	1	fveq2i	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩ )
3		prex	⊢ { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ∈ V
4		opvtxfv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ∈ V ) → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩ ) = 𝑉 )
5	3 4	mpan2	⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ ⟨ 𝑉 , { ⟨ 0 , { 𝐴 , 𝐵 } ⟩ , ⟨ 1 , { 𝐴 , 𝐵 } ⟩ } ⟩ ) = 𝑉 )
6	2 5	eqtrid	⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 )