Theorem uspgrloopiedg

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, 21-Feb-2021)

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

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	⊢ 𝐺 = ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩
2	1	fveq2i	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩ )
3		snex	⊢ { ⟨ 𝐴 , { 𝑁 } ⟩ } ∈ V
4	3	a1i	⊢ ( 𝐴 ∈ 𝑋 → { ⟨ 𝐴 , { 𝑁 } ⟩ } ∈ V )
5		opiedgfv	⊢ ( ( 𝑉 ∈ 𝑊 ∧ { ⟨ 𝐴 , { 𝑁 } ⟩ } ∈ V ) → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩ ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
6	4 5	sylan2	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ( iEdg ‘ ⟨ 𝑉 , { ⟨ 𝐴 , { 𝑁 } ⟩ } ⟩ ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )
7	2 6	eqtrid	⊢ ( ( 𝑉 ∈ 𝑊 ∧ 𝐴 ∈ 𝑋 ) → ( iEdg ‘ 𝐺 ) = { ⟨ 𝐴 , { 𝑁 } ⟩ } )