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

Metamath Proof Explorer

Theorem uspgrloopedg

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

Ref Expression
Hypothesis uspgrloopvtx.g ⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
Assertion uspgrloopedg ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ( Edg ‘ 𝐺 ) = { { 𝑁 } } )

Proof

Step Hyp Ref Expression
1 uspgrloopvtx.g ⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
2 1 fveq2i ⊢ ( Edg ‘ 𝐺 ) = ( Edg ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩ )
3 snex ⊢ { ⟨ 𝐴 , { 𝑁 } ⟩ } ∈ V
4 3 a1i ⊢ ( 𝐴 ∈ 𝑋 → { ⟨ 𝐴 , { 𝑁 } ⟩ } ∈ V )
5 edgopval ⊢ ( ( 𝑉 ∈ 𝑊 ∧ { ⟨ 𝐴 , { 𝑁 } ⟩ } ∈ V ) → ( Edg ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩ ) = ran { ⟨ 𝐴 , { 𝑁 } ⟩ } )
6 4 5 sylan2 ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ( Edg ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩ ) = ran { ⟨ 𝐴 , { 𝑁 } ⟩ } )
7 2 6 eqtrid ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ( Edg ‘ 𝐺 ) = ran { ⟨ 𝐴 , { 𝑁 } ⟩ } )
8 rnsnopg ⊢ ( 𝐴 ∈ 𝑋 → ran { ⟨ 𝐴 , { 𝑁 } ⟩ } = { { 𝑁 } } )
9 8 adantl ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ran { ⟨ 𝐴 , { 𝑁 } ⟩ } = { { 𝑁 } } )
10 7 9 eqtrd ⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ( Edg ‘ 𝐺 ) = { { 𝑁 } } )