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	$⊢ G = ⟨V, \{⟨A, \{N\}⟩\}⟩$
	Assertion	uspgrloopedg	$⊢ (V \in W \land A \in X) \to Edg (G) = \{\{N\}\}$

Proof

Step	Hyp	Ref	Expression
1		uspgrloopvtx.g	$⊢ G = ⟨V, \{⟨A, \{N\}⟩\}⟩$
2	1	fveq2i	$⊢ Edg (G) = Edg (⟨V, \{⟨A, \{N\}⟩\}⟩)$
3		snex	$⊢ \{⟨A, \{N\}⟩\} \in V$
4	3	a1i	$⊢ A \in X \to \{⟨A, \{N\}⟩\} \in V$
5		edgopval	$⊢ (V \in W \land \{⟨A, \{N\}⟩\} \in V) \to Edg (⟨V, \{⟨A, \{N\}⟩\}⟩) = ran \{⟨A, \{N\}⟩\}$
6	4 5	sylan2	$⊢ (V \in W \land A \in X) \to Edg (⟨V, \{⟨A, \{N\}⟩\}⟩) = ran \{⟨A, \{N\}⟩\}$
7	2 6	eqtrid	$⊢ (V \in W \land A \in X) \to Edg (G) = ran \{⟨A, \{N\}⟩\}$
8		rnsnopg	$⊢ A \in X \to ran \{⟨A, \{N\}⟩\} = \{\{N\}\}$
9	8	adantl	$⊢ (V \in W \land A \in X) \to ran \{⟨A, \{N\}⟩\} = \{\{N\}\}$
10	7 9	eqtrd	$⊢ (V \in W \land A \in X) \to Edg (G) = \{\{N\}\}$