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	syl5eq	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ( Edg ‘ 𝐺 ) = ran { ⟨ 𝐴 , { 𝑁 } ⟩ } )
8		rnsnopg	⊢ ( 𝐴 ∈ 𝑋 → ran { ⟨ 𝐴 , { 𝑁 } ⟩ } = { { 𝑁 } } )
9	8	adantl	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ran { ⟨ 𝐴 , { 𝑁 } ⟩ } = { { 𝑁 } } )
10	7 9	eqtrd	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ( Edg ‘ 𝐺 ) = { { 𝑁 } } )