Theorem 1loopgredg

Description: The set of edges in a graph (simple pseudograph) with one edge which is a loop is a singleton of a singleton. (Contributed by AV, 17-Dec-2020) (Revised by AV, 21-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		1loopgruspgr.v	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
2		1loopgruspgr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3		1loopgruspgr.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
4		1loopgruspgr.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
5		edgval	⊢ ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 )
6	5	a1i	⊢ ( 𝜑 → ( Edg ‘ 𝐺 ) = ran ( iEdg ‘ 𝐺 ) )
7	4	rneqd	⊢ ( 𝜑 → ran ( iEdg ‘ 𝐺 ) = ran { ⟨ 𝐴 , { 𝑁 } ⟩ } )
8		rnsnopg	⊢ ( 𝐴 ∈ 𝑋 → ran { ⟨ 𝐴 , { 𝑁 } ⟩ } = { { 𝑁 } } )
9	2 8	syl	⊢ ( 𝜑 → ran { ⟨ 𝐴 , { 𝑁 } ⟩ } = { { 𝑁 } } )
10	6 7 9	3eqtrd	⊢ ( 𝜑 → ( Edg ‘ 𝐺 ) = { { 𝑁 } } )