Description: A vertex 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 | umgr2v2evtxel | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | umgr2v2evtx.g | ⊢ 𝐺 = 〈 𝑉 , { 〈 0 , { 𝐴 , 𝐵 } 〉 , 〈 1 , { 𝐴 , 𝐵 } 〉 } 〉 | |
2 | 1 | umgr2v2evtx | ⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 ) |
3 | eqcom | ⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 ↔ 𝑉 = ( Vtx ‘ 𝐺 ) ) | |
4 | 3 | biimpi | ⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 → 𝑉 = ( Vtx ‘ 𝐺 ) ) |
5 | 4 | eleq2d | ⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( 𝐴 ∈ 𝑉 ↔ 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ) |
6 | 5 | biimpcd | ⊢ ( 𝐴 ∈ 𝑉 → ( ( Vtx ‘ 𝐺 ) = 𝑉 → 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) ) |
7 | 2 6 | mpan9 | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → 𝐴 ∈ ( Vtx ‘ 𝐺 ) ) |