Theorem 1loopgrvd2

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, 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, 21-Feb-2021)

	Ref	Expression
Hypotheses	1loopgruspgr.v	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
	1loopgruspgr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	1loopgruspgr.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
	1loopgruspgr.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
Assertion	1loopgrvd2	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = 2 )

Proof

Step	Hyp	Ref	Expression
1		1loopgruspgr.v	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
2		1loopgruspgr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3		1loopgruspgr.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
4		1loopgruspgr.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
5	1 2 3 4	1loopgruspgr	⊢ ( 𝜑 → 𝐺 ∈ USPGraph )
6		uspgrushgr	⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ USHGraph )
7	5 6	syl	⊢ ( 𝜑 → 𝐺 ∈ USHGraph )
8	3 1	eleqtrrd	⊢ ( 𝜑 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
9		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
10		eqid	⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ 𝐺 )
11		eqid	⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
12	9 10 11	vtxdushgrfvedg	⊢ ( ( 𝐺 ∈ USHGraph ∧ 𝑁 ∈ ( Vtx ‘ 𝐺 ) ) → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) ) )
13	7 8 12	syl2anc	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) ) )
14		snex	⊢ { 𝑁 } ∈ V
15		sneq	⊢ ( 𝑎 = { 𝑁 } → { 𝑎 } = { { 𝑁 } } )
16	15	eqeq2d	⊢ ( 𝑎 = { 𝑁 } → ( { { 𝑁 } } = { 𝑎 } ↔ { { 𝑁 } } = { { 𝑁 } } ) )
17		eqid	⊢ { { 𝑁 } } = { { 𝑁 } }
18	14 16 17	ceqsexv2d	⊢ ∃ 𝑎 { { 𝑁 } } = { 𝑎 }
19	18	a1i	⊢ ( 𝜑 → ∃ 𝑎 { { 𝑁 } } = { 𝑎 } )
20		snidg	⊢ ( 𝑁 ∈ 𝑉 → 𝑁 ∈ { 𝑁 } )
21	3 20	syl	⊢ ( 𝜑 → 𝑁 ∈ { 𝑁 } )
22	21	iftrued	⊢ ( 𝜑 → if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { { 𝑁 } } )
23	22	eqeq1d	⊢ ( 𝜑 → ( if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ { { 𝑁 } } = { 𝑎 } ) )
24	23	exbidv	⊢ ( 𝜑 → ( ∃ 𝑎 if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ ∃ 𝑎 { { 𝑁 } } = { 𝑎 } ) )
25	19 24	mpbird	⊢ ( 𝜑 → ∃ 𝑎 if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } )
26	1 2 3 4	1loopgredg	⊢ ( 𝜑 → ( Edg ‘ 𝐺 ) = { { 𝑁 } } )
27	26	rabeqdv	⊢ ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑒 ∈ { { 𝑁 } } ∣ 𝑁 ∈ 𝑒 } )
28		eleq2	⊢ ( 𝑒 = { 𝑁 } → ( 𝑁 ∈ 𝑒 ↔ 𝑁 ∈ { 𝑁 } ) )
29	28	rabsnif	⊢ { 𝑒 ∈ { { 𝑁 } } ∣ 𝑁 ∈ 𝑒 } = if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ )
30	27 29	eqtrdi	⊢ ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) )
31	30	eqeq1d	⊢ ( 𝜑 → ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑎 } ↔ if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) )
32	31	exbidv	⊢ ( 𝜑 → ( ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑎 } ↔ ∃ 𝑎 if ( 𝑁 ∈ { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) )
33	25 32	mpbird	⊢ ( 𝜑 → ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑎 } )
34		fvex	⊢ ( Edg ‘ 𝐺 ) ∈ V
35	34	rabex	⊢ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ∈ V
36		hash1snb	⊢ ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ∈ V → ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑎 } ) )
37	35 36	ax-mp	⊢ ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } = { 𝑎 } )
38	33 37	sylibr	⊢ ( 𝜑 → ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) = 1 )
39		eqid	⊢ { 𝑁 } = { 𝑁 }
40	39	iftruei	⊢ if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { { 𝑁 } }
41	40	eqeq1i	⊢ ( if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ { { 𝑁 } } = { 𝑎 } )
42	41	exbii	⊢ ( ∃ 𝑎 if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ↔ ∃ 𝑎 { { 𝑁 } } = { 𝑎 } )
43	19 42	sylibr	⊢ ( 𝜑 → ∃ 𝑎 if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } )
44	26	rabeqdv	⊢ ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑒 ∈ { { 𝑁 } } ∣ 𝑒 = { 𝑁 } } )
45		eqeq1	⊢ ( 𝑒 = { 𝑁 } → ( 𝑒 = { 𝑁 } ↔ { 𝑁 } = { 𝑁 } ) )
46	45	rabsnif	⊢ { 𝑒 ∈ { { 𝑁 } } ∣ 𝑒 = { 𝑁 } } = if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ )
47	44 46	eqtrdi	⊢ ( 𝜑 → { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) )
48	47	eqeq1d	⊢ ( 𝜑 → ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } ↔ if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) )
49	48	exbidv	⊢ ( 𝜑 → ( ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } ↔ ∃ 𝑎 if ( { 𝑁 } = { 𝑁 } , { { 𝑁 } } , ∅ ) = { 𝑎 } ) )
50	43 49	mpbird	⊢ ( 𝜑 → ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } )
51	34	rabex	⊢ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ∈ V
52		hash1snb	⊢ ( { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ∈ V → ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } ) )
53	51 52	ax-mp	⊢ ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) = 1 ↔ ∃ 𝑎 { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } = { 𝑎 } )
54	50 53	sylibr	⊢ ( 𝜑 → ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) = 1 )
55	38 54	oveq12d	⊢ ( 𝜑 → ( ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑁 ∈ 𝑒 } ) +𝑒 ( ♯ ‘ { 𝑒 ∈ ( Edg ‘ 𝐺 ) ∣ 𝑒 = { 𝑁 } } ) ) = ( 1 +𝑒 1 ) )
56		1re	⊢ 1 ∈ ℝ
57		rexadd	⊢ ( ( 1 ∈ ℝ ∧ 1 ∈ ℝ ) → ( 1 +𝑒 1 ) = ( 1 + 1 ) )
58	56 56 57	mp2an	⊢ ( 1 +𝑒 1 ) = ( 1 + 1 )
59		1p1e2	⊢ ( 1 + 1 ) = 2
60	58 59	eqtri	⊢ ( 1 +𝑒 1 ) = 2
61	60	a1i	⊢ ( 𝜑 → ( 1 +𝑒 1 ) = 2 )
62	13 55 61	3eqtrd	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝑁 ) = 2 )