Theorem 1loopgruspgr

Description: A graph with one edge which is a loop is a simple pseudograph (see also uspgr1v1eop ). (Contributed by AV, 21-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		1loopgruspgr.v	⊢ ( 𝜑 → ( Vtx ‘ 𝐺 ) = 𝑉 )
2		1loopgruspgr.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑋 )
3		1loopgruspgr.n	⊢ ( 𝜑 → 𝑁 ∈ 𝑉 )
4		1loopgruspgr.i	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
5		eqid	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ 𝐺 )
6	3 1	eleqtrrd	⊢ ( 𝜑 → 𝑁 ∈ ( Vtx ‘ 𝐺 ) )
7		dfsn2	⊢ { 𝑁 } = { 𝑁 , 𝑁 }
8	7	a1i	⊢ ( 𝜑 → { 𝑁 } = { 𝑁 , 𝑁 } )
9	8	opeq2d	⊢ ( 𝜑 → ⟨ 𝐴 , { 𝑁 } ⟩ = ⟨ 𝐴 , { 𝑁 , 𝑁 } ⟩ )
10	9	sneqd	⊢ ( 𝜑 → { ⟨ 𝐴 , { 𝑁 } ⟩ } = { ⟨ 𝐴 , { 𝑁 , 𝑁 } ⟩ } )
11	4 10	eqtrd	⊢ ( 𝜑 → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 , 𝑁 } ⟩ } )
12	5 2 6 6 11	uspgr1e	⊢ ( 𝜑 → 𝐺 ∈ USPGraph )