1egrvtxdg0

Description: The vertex degree of a one-edge graph, case 1: an edge between two vertices other than the given vertex contributes nothing to the vertex degree. (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Alexander van der Vekens, 22-Dec-2017) (Revised by AV, 21-Feb-2021)

	Ref	Expression
Hypotheses	1egrvtxdg1.v	$⊢ φ \to Vtx (G) = V$
	1egrvtxdg1.a	$⊢ φ \to A \in X$
	1egrvtxdg1.b	$⊢ φ \to B \in V$
	1egrvtxdg1.c	$⊢ φ \to C \in V$
	1egrvtxdg1.n	$⊢ φ \to B \neq C$
	1egrvtxdg0.d	$⊢ φ \to D \in V$
	1egrvtxdg0.n	$⊢ φ \to C \neq D$
	1egrvtxdg0.i	$⊢ φ \to iEdg (G) = \{⟨A, \{B, D\}⟩\}$
Assertion	1egrvtxdg0	$⊢ φ \to VtxDeg (G) (C) = 0$

Proof

Step	Hyp	Ref	Expression
1		1egrvtxdg1.v	$⊢ φ \to Vtx (G) = V$
2		1egrvtxdg1.a	$⊢ φ \to A \in X$
3		1egrvtxdg1.b	$⊢ φ \to B \in V$
4		1egrvtxdg1.c	$⊢ φ \to C \in V$
5		1egrvtxdg1.n	$⊢ φ \to B \neq C$
6		1egrvtxdg0.d	$⊢ φ \to D \in V$
7		1egrvtxdg0.n	$⊢ φ \to C \neq D$
8		1egrvtxdg0.i	$⊢ φ \to iEdg (G) = \{⟨A, \{B, D\}⟩\}$
9	1	adantl	$⊢ (B = D \land φ) \to Vtx (G) = V$
10	2	adantl	$⊢ (B = D \land φ) \to A \in X$
11	3	adantl	$⊢ (B = D \land φ) \to B \in V$
12	8	adantl	$⊢ (B = D \land φ) \to iEdg (G) = \{⟨A, \{B, D\}⟩\}$
13		preq2	$⊢ D = B \to \{B, D\} = \{B, B\}$
14	13	eqcoms	$⊢ B = D \to \{B, D\} = \{B, B\}$
15		dfsn2	$⊢ \{B\} = \{B, B\}$
16	14 15	eqtr4di	$⊢ B = D \to \{B, D\} = \{B\}$
17	16	adantr	$⊢ (B = D \land φ) \to \{B, D\} = \{B\}$
18	17	opeq2d	$⊢ (B = D \land φ) \to ⟨A, \{B, D\}⟩ = ⟨A, \{B\}⟩$
19	18	sneqd	$⊢ (B = D \land φ) \to \{⟨A, \{B, D\}⟩\} = \{⟨A, \{B\}⟩\}$
20	12 19	eqtrd	$⊢ (B = D \land φ) \to iEdg (G) = \{⟨A, \{B\}⟩\}$
21	5	necomd	$⊢ φ \to C \neq B$
22	4 21	jca	$⊢ φ \to (C \in V \land C \neq B)$
23		eldifsn	$⊢ C \in (V ∖ \{B\}) \leftrightarrow (C \in V \land C \neq B)$
24	22 23	sylibr	$⊢ φ \to C \in (V ∖ \{B\})$
25	24	adantl	$⊢ (B = D \land φ) \to C \in (V ∖ \{B\})$
26	9 10 11 20 25	1loopgrvd0	$⊢ (B = D \land φ) \to VtxDeg (G) (C) = 0$
27	26	ex	$⊢ B = D \to (φ \to VtxDeg (G) (C) = 0)$
28		necom	$⊢ B \neq C \leftrightarrow C \neq B$
29		df-ne	$⊢ C \neq B \leftrightarrow \neg C = B$
30	28 29	sylbb	$⊢ B \neq C \to \neg C = B$
31	5 30	syl	$⊢ φ \to \neg C = B$
32	7	neneqd	$⊢ φ \to \neg C = D$
33	31 32	jca	$⊢ φ \to (\neg C = B \land \neg C = D)$
34	33	adantl	$⊢ (B \neq D \land φ) \to (\neg C = B \land \neg C = D)$
35		ioran	$⊢ \neg (C = B \lor C = D) \leftrightarrow (\neg C = B \land \neg C = D)$
36	34 35	sylibr	$⊢ (B \neq D \land φ) \to \neg (C = B \lor C = D)$
37		edgval	$⊢ Edg (G) = ran iEdg (G)$
38	8	rneqd	$⊢ φ \to ran iEdg (G) = ran \{⟨A, \{B, D\}⟩\}$
39		rnsnopg	$⊢ A \in X \to ran \{⟨A, \{B, D\}⟩\} = \{\{B, D\}\}$
40	2 39	syl	$⊢ φ \to ran \{⟨A, \{B, D\}⟩\} = \{\{B, D\}\}$
41	38 40	eqtrd	$⊢ φ \to ran iEdg (G) = \{\{B, D\}\}$
42	37 41	eqtrid	$⊢ φ \to Edg (G) = \{\{B, D\}\}$
43	42	adantl	$⊢ (B \neq D \land φ) \to Edg (G) = \{\{B, D\}\}$
44	43	rexeqdv	$⊢ (B \neq D \land φ) \to (\exists e \in Edg (G) C \in e \leftrightarrow \exists e \in \{\{B, D\}\} C \in e)$
45		prex	$⊢ \{B, D\} \in V$
46		eleq2	$⊢ e = \{B, D\} \to (C \in e \leftrightarrow C \in \{B, D\})$
47	46	rexsng	$⊢ \{B, D\} \in V \to (\exists e \in \{\{B, D\}\} C \in e \leftrightarrow C \in \{B, D\})$
48	45 47	mp1i	$⊢ (B \neq D \land φ) \to (\exists e \in \{\{B, D\}\} C \in e \leftrightarrow C \in \{B, D\})$
49		elprg	$⊢ C \in V \to (C \in \{B, D\} \leftrightarrow (C = B \lor C = D))$
50	4 49	syl	$⊢ φ \to (C \in \{B, D\} \leftrightarrow (C = B \lor C = D))$
51	50	adantl	$⊢ (B \neq D \land φ) \to (C \in \{B, D\} \leftrightarrow (C = B \lor C = D))$
52	44 48 51	3bitrd	$⊢ (B \neq D \land φ) \to (\exists e \in Edg (G) C \in e \leftrightarrow (C = B \lor C = D))$
53	36 52	mtbird	$⊢ (B \neq D \land φ) \to \neg \exists e \in Edg (G) C \in e$
54		eqid	$⊢ Vtx (G) = Vtx (G)$
55	2	adantl	$⊢ (B \neq D \land φ) \to A \in X$
56	3 1	eleqtrrd	$⊢ φ \to B \in Vtx (G)$
57	56	adantl	$⊢ (B \neq D \land φ) \to B \in Vtx (G)$
58	6 1	eleqtrrd	$⊢ φ \to D \in Vtx (G)$
59	58	adantl	$⊢ (B \neq D \land φ) \to D \in Vtx (G)$
60	8	adantl	$⊢ (B \neq D \land φ) \to iEdg (G) = \{⟨A, \{B, D\}⟩\}$
61		simpl	$⊢ (B \neq D \land φ) \to B \neq D$
62	54 55 57 59 60 61	usgr1e	$⊢ (B \neq D \land φ) \to G \in USGraph$
63	4 1	eleqtrrd	$⊢ φ \to C \in Vtx (G)$
64	63	adantl	$⊢ (B \neq D \land φ) \to C \in Vtx (G)$
65		eqid	$⊢ Edg (G) = Edg (G)$
66		eqid	$⊢ VtxDeg (G) = VtxDeg (G)$
67	54 65 66	vtxdusgr0edgnel	$⊢ (G \in USGraph \land C \in Vtx (G)) \to (VtxDeg (G) (C) = 0 \leftrightarrow \neg \exists e \in Edg (G) C \in e)$
68	62 64 67	syl2anc	$⊢ (B \neq D \land φ) \to (VtxDeg (G) (C) = 0 \leftrightarrow \neg \exists e \in Edg (G) C \in e)$
69	53 68	mpbird	$⊢ (B \neq D \land φ) \to VtxDeg (G) (C) = 0$
70	69	ex	$⊢ B \neq D \to (φ \to VtxDeg (G) (C) = 0)$
71	27 70	pm2.61ine	$⊢ φ \to VtxDeg (G) (C) = 0$

Metamath Proof Explorer

Theorem 1egrvtxdg0

Proof