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

Metamath Proof Explorer

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 ‘ 𝐺 ) = { { 𝑁 } } )