Description: A vertex in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop ). (Contributed by AV, 17-Dec-2020)
Ref | Expression | ||
---|---|---|---|
Hypothesis | uspgrloopvtx.g | ⊢ 𝐺 = 〈 𝑉 , { 〈 𝐴 , { 𝑁 } 〉 } 〉 | |
Assertion | uspgrloopvtxel | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | uspgrloopvtx.g | ⊢ 𝐺 = 〈 𝑉 , { 〈 𝐴 , { 𝑁 } 〉 } 〉 | |
2 | 1 | uspgrloopvtx | ⊢ ( 𝑉 ∈ 𝑊 → ( Vtx ‘ 𝐺 ) = 𝑉 ) |
3 | eleq2 | ⊢ ( 𝑉 = ( Vtx ‘ 𝐺 ) → ( 𝑁 ∈ 𝑉 ↔ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) | |
4 | 3 | biimpd | ⊢ ( 𝑉 = ( Vtx ‘ 𝐺 ) → ( 𝑁 ∈ 𝑉 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) |
5 | 4 | eqcoms | ⊢ ( ( Vtx ‘ 𝐺 ) = 𝑉 → ( 𝑁 ∈ 𝑉 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) |
6 | 5 | com12 | ⊢ ( 𝑁 ∈ 𝑉 → ( ( Vtx ‘ 𝐺 ) = 𝑉 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) ) |
7 | 2 6 | mpan9 | ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝑁 ∈ 𝑉 ) → 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) |