uspgrloopvd2

Description: The vertex degree of a one-edge graph, case 4: an edge from a vertex to itself contributes two to the vertex's degree. I. e. in a graph (simple pseudograph) with one edge which is a loop (see uspgr1v1eop ), the vertex connected with itself by the loop has degree 2. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 22-Dec-2017) (Revised by AV, 17-Dec-2020) (Proof shortened by AV, 21-Feb-2021)

		Ref	Expression
	Hypothesis	uspgrloopvtx.g	$⊢ G = ⟨V, \{⟨A, \{N\}⟩\}⟩$
	Assertion	uspgrloopvd2	$⊢ (V \in W \land A \in X \land N \in V) \to VtxDeg (G) (N) = 2$

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	$⊢ G = ⟨V, \{⟨A, \{N\}⟩\}⟩$
2	1	uspgrloopvtx	$⊢ V \in W \to Vtx (G) = V$
3	2	3ad2ant1	$⊢ (V \in W \land A \in X \land N \in V) \to Vtx (G) = V$
4		simp2	$⊢ (V \in W \land A \in X \land N \in V) \to A \in X$
5		simp3	$⊢ (V \in W \land A \in X \land N \in V) \to N \in V$
6	1	uspgrloopiedg	$⊢ (V \in W \land A \in X) \to iEdg (G) = \{⟨A, \{N\}⟩\}$
7	6	3adant3	$⊢ (V \in W \land A \in X \land N \in V) \to iEdg (G) = \{⟨A, \{N\}⟩\}$
8	3 4 5 7	1loopgrvd2	$⊢ (V \in W \land A \in X \land N \in V) \to VtxDeg (G) (N) = 2$

Metamath Proof Explorer

Theorem uspgrloopvd2

Proof