This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )