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

Metamath Proof Explorer

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	\|- G = <. V , { <. A , { N } >. } >.
	Assertion	uspgrloopiedg	\|- ( ( V e. W /\ A e. X ) -> ( iEdg ` G ) = { <. A , { N } >. } )

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	\|- G = <. V , { <. A , { N } >. } >.
2	1	fveq2i	\|- ( iEdg ` G ) = ( iEdg ` <. V , { <. A , { N } >. } >. )
3		snex	\|- { <. A , { N } >. } e. _V
4	3	a1i	\|- ( A e. X -> { <. A , { N } >. } e. _V )
5		opiedgfv	\|- ( ( V e. W /\ { <. A , { N } >. } e. _V ) -> ( iEdg ` <. V , { <. A , { N } >. } >. ) = { <. A , { N } >. } )
6	4 5	sylan2	\|- ( ( V e. W /\ A e. X ) -> ( iEdg ` <. V , { <. A , { N } >. } >. ) = { <. A , { N } >. } )
7	2 6	eqtrid	\|- ( ( V e. W /\ A e. X ) -> ( iEdg ` G ) = { <. A , { N } >. } )