1loopgrvd0

Description: The vertex degree of a one-edge graph, case 1 (for a loop): a loop at a vertex other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by AV, 21-Feb-2021)

	Ref	Expression
Hypotheses	1loopgruspgr.v	$⊢ φ \to Vtx (G) = V$
	1loopgruspgr.a	$⊢ φ \to A \in X$
	1loopgruspgr.n	$⊢ φ \to N \in V$
	1loopgruspgr.i	$⊢ φ \to iEdg (G) = \{⟨A, \{N\}⟩\}$
	1loopgrvd0.k	$⊢ φ \to K \in (V ∖ \{N\})$
Assertion	1loopgrvd0	$⊢ φ \to VtxDeg (G) (K) = 0$

Proof

Step	Hyp	Ref	Expression
1		1loopgruspgr.v	$⊢ φ \to Vtx (G) = V$
2		1loopgruspgr.a	$⊢ φ \to A \in X$
3		1loopgruspgr.n	$⊢ φ \to N \in V$
4		1loopgruspgr.i	$⊢ φ \to iEdg (G) = \{⟨A, \{N\}⟩\}$
5		1loopgrvd0.k	$⊢ φ \to K \in (V ∖ \{N\})$
6	5	eldifbd	$⊢ φ \to \neg K \in \{N\}$
7		snex	$⊢ \{N\} \in V$
8		fvsng	$⊢ (A \in X \land \{N\} \in V) \to \{⟨A, \{N\}⟩\} (A) = \{N\}$
9	2 7 8	sylancl	$⊢ φ \to \{⟨A, \{N\}⟩\} (A) = \{N\}$
10	9	eleq2d	$⊢ φ \to (K \in \{⟨A, \{N\}⟩\} (A) \leftrightarrow K \in \{N\})$
11	6 10	mtbird	$⊢ φ \to \neg K \in \{⟨A, \{N\}⟩\} (A)$
12	4	dmeqd	$⊢ φ \to dom iEdg (G) = dom \{⟨A, \{N\}⟩\}$
13		dmsnopg	$⊢ \{N\} \in V \to dom \{⟨A, \{N\}⟩\} = \{A\}$
14	7 13	mp1i	$⊢ φ \to dom \{⟨A, \{N\}⟩\} = \{A\}$
15	12 14	eqtrd	$⊢ φ \to dom iEdg (G) = \{A\}$
16	4	fveq1d	$⊢ φ \to iEdg (G) (i) = \{⟨A, \{N\}⟩\} (i)$
17	16	eleq2d	$⊢ φ \to (K \in iEdg (G) (i) \leftrightarrow K \in \{⟨A, \{N\}⟩\} (i))$
18	15 17	rexeqbidv	$⊢ φ \to (\exists i \in dom iEdg (G) K \in iEdg (G) (i) \leftrightarrow \exists i \in \{A\} K \in \{⟨A, \{N\}⟩\} (i))$
19		fveq2	$⊢ i = A \to \{⟨A, \{N\}⟩\} (i) = \{⟨A, \{N\}⟩\} (A)$
20	19	eleq2d	$⊢ i = A \to (K \in \{⟨A, \{N\}⟩\} (i) \leftrightarrow K \in \{⟨A, \{N\}⟩\} (A))$
21	20	rexsng	$⊢ A \in X \to (\exists i \in \{A\} K \in \{⟨A, \{N\}⟩\} (i) \leftrightarrow K \in \{⟨A, \{N\}⟩\} (A))$
22	2 21	syl	$⊢ φ \to (\exists i \in \{A\} K \in \{⟨A, \{N\}⟩\} (i) \leftrightarrow K \in \{⟨A, \{N\}⟩\} (A))$
23	18 22	bitrd	$⊢ φ \to (\exists i \in dom iEdg (G) K \in iEdg (G) (i) \leftrightarrow K \in \{⟨A, \{N\}⟩\} (A))$
24	11 23	mtbird	$⊢ φ \to \neg \exists i \in dom iEdg (G) K \in iEdg (G) (i)$
25	5	eldifad	$⊢ φ \to K \in V$
26	1	eleq2d	$⊢ φ \to (K \in Vtx (G) \leftrightarrow K \in V)$
27	25 26	mpbird	$⊢ φ \to K \in Vtx (G)$
28		eqid	$⊢ Vtx (G) = Vtx (G)$
29		eqid	$⊢ iEdg (G) = iEdg (G)$
30		eqid	$⊢ VtxDeg (G) = VtxDeg (G)$
31	28 29 30	vtxd0nedgb	$⊢ K \in Vtx (G) \to (VtxDeg (G) (K) = 0 \leftrightarrow \neg \exists i \in dom iEdg (G) K \in iEdg (G) (i))$
32	27 31	syl	$⊢ φ \to (VtxDeg (G) (K) = 0 \leftrightarrow \neg \exists i \in dom iEdg (G) K \in iEdg (G) (i))$
33	24 32	mpbird	$⊢ φ \to VtxDeg (G) (K) = 0$

Metamath Proof Explorer

Theorem 1loopgrvd0

Proof