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

Metamath Proof Explorer

Theorem 1loopgredg

Description: The set of edges in a graph (simple pseudograph) with one edge which is a loop is a singleton of a singleton. (Contributed by AV, 17-Dec-2020) (Revised by AV, 21-Feb-2021)

		Ref	Expression
	Hypotheses	1loopgruspgr.v	$⊢ φ \to Vtx (G) = V$
		1loopgruspgr.a	$⊢ φ \to A \in X$
		1loopgruspgr.n	$⊢ φ \to N \in V$
		1loopgruspgr.i	$⊢ φ \to iEdg (G) = \{⟨A, \{N\}⟩\}$
	Assertion	1loopgredg	$⊢ φ \to Edg (G) = \{\{N\}\}$

Proof

Step	Hyp	Ref	Expression
1		1loopgruspgr.v	$⊢ φ \to Vtx (G) = V$
2		1loopgruspgr.a	$⊢ φ \to A \in X$
3		1loopgruspgr.n	$⊢ φ \to N \in V$
4		1loopgruspgr.i	$⊢ φ \to iEdg (G) = \{⟨A, \{N\}⟩\}$
5		edgval	$⊢ Edg (G) = ran iEdg (G)$
6	5	a1i	$⊢ φ \to Edg (G) = ran iEdg (G)$
7	4	rneqd	$⊢ φ \to ran iEdg (G) = ran \{⟨A, \{N\}⟩\}$
8		rnsnopg	$⊢ A \in X \to ran \{⟨A, \{N\}⟩\} = \{\{N\}\}$
9	2 8	syl	$⊢ φ \to ran \{⟨A, \{N\}⟩\} = \{\{N\}\}$
10	6 7 9	3eqtrd	$⊢ φ \to Edg (G) = \{\{N\}\}$