Theorem 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	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
	1egrvtxdg1.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	1egrvtxdg1.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
	1egrvtxdg1.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑉 )
	1egrvtxdg1.n	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
	1egrvtxdg0.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑉 )
	1egrvtxdg0.n	⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
	1egrvtxdg0.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝐵 , 𝐷 } ⟩ } )
Assertion	1egrvtxdg0	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐶 ) = 0 )

Proof

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