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 \in W \land A \in X) \to 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\}⟩\} \in V$
4	3	a1i	$⊢ A \in X \to \{⟨A, \{N\}⟩\} \in V$
5		opiedgfv	$⊢ (V \in W \land \{⟨A, \{N\}⟩\} \in V) \to iEdg (⟨V, \{⟨A, \{N\}⟩\}⟩) = \{⟨A, \{N\}⟩\}$
6	4 5	sylan2	$⊢ (V \in W \land A \in X) \to iEdg (⟨V, \{⟨A, \{N\}⟩\}⟩) = \{⟨A, \{N\}⟩\}$
7	2 6	eqtrid	$⊢ (V \in W \land A \in X) \to iEdg (G) = \{⟨A, \{N\}⟩\}$