Theorem 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	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
	1loopgruspgr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
	1loopgruspgr.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
	1loopgruspgr.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
	1loopgrvd0.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) )
Assertion	1loopgrvd0	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐾 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		1loopgruspgr.v	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
2		1loopgruspgr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3		1loopgruspgr.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
4		1loopgruspgr.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
5		1loopgrvd0.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑉 ∖ { 𝑁 } ) )
6	5	eldifbd	⊢ ( 𝜑 → ¬ 𝐾 ∈ { 𝑁 } )
7		snex	⊢ { 𝑁 } ∈ V
8		fvsng	⊢ ( ( 𝐴 ∈ 𝑋 ∧ { 𝑁 } ∈ V ) → ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) = { 𝑁 } )
9	2 7 8	sylancl	⊢ ( 𝜑 → ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) = { 𝑁 } )
10	9	eleq2d	⊢ ( 𝜑 → ( 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) ↔ 𝐾 ∈ { 𝑁 } ) )
11	6 10	mtbird	⊢ ( 𝜑 → ¬ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) )
12	4	dmeqd	⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = dom { ⟨ 𝐴 , { 𝑁 } ⟩ } )
13		dmsnopg	⊢ ( { 𝑁 } ∈ V → dom { ⟨ 𝐴 , { 𝑁 } ⟩ } = { 𝐴 } )
14	7 13	mp1i	⊢ ( 𝜑 → dom { ⟨ 𝐴 , { 𝑁 } ⟩ } = { 𝐴 } )
15	12 14	eqtrd	⊢ ( 𝜑 → dom ( iEdg ‘ 𝐺 ) = { 𝐴 } )
16	4	fveq1d	⊢ ( 𝜑 → ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) = ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) )
17	16	eleq2d	⊢ ( 𝜑 → ( 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ↔ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) ) )
18	15 17	rexeqbidv	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ↔ ∃ 𝑖 ∈ { 𝐴 } 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) ) )
19		fveq2	⊢ ( 𝑖 = 𝐴 → ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) = ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) )
20	19	eleq2d	⊢ ( 𝑖 = 𝐴 → ( 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) ↔ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) ) )
21	20	rexsng	⊢ ( 𝐴 ∈ 𝑋 → ( ∃ 𝑖 ∈ { 𝐴 } 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) ↔ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) ) )
22	2 21	syl	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ { 𝐴 } 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝑖 ) ↔ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) ) )
23	18 22	bitrd	⊢ ( 𝜑 → ( ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ↔ 𝐾 ∈ ( { ⟨ 𝐴 , { 𝑁 } ⟩ } ‘ 𝐴 ) ) )
24	11 23	mtbird	⊢ ( 𝜑 → ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) )
25	5	eldifad	⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
26	1	eleq2d	⊢ ( 𝜑 → ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) ↔ 𝐾 ∈ 𝑉 ) )
27	25 26	mpbird	⊢ ( 𝜑 → 𝐾 ∈ ( Vtx ‘ 𝐺 ) )
28		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
29		eqid	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ 𝐺 )
30		eqid	⊢ ( VtxDeg ‘ 𝐺 ) = ( VtxDeg ‘ 𝐺 )
31	28 29 30	vtxd0nedgb	⊢ ( 𝐾 ∈ ( Vtx ‘ 𝐺 ) → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐾 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
32	27 31	syl	⊢ ( 𝜑 → ( ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐾 ) = 0 ↔ ¬ ∃ 𝑖 ∈ dom ( iEdg ‘ 𝐺 ) 𝐾 ∈ ( ( iEdg ‘ 𝐺 ) ‘ 𝑖 ) ) )
33	24 32	mpbird	⊢ ( 𝜑 → ( ( VtxDeg ‘ 𝐺 ) ‘ 𝐾 ) = 0 )