umgrnloop2

Description: A multigraph has no loops. (Contributed by AV, 27-Oct-2020) (Revised by AV, 30-Nov-2020)

		Ref	Expression
	Assertion	umgrnloop2	$⊢ G \in UMGraph \to \{N, N\} \notin Edg (G)$

Step	Hyp	Ref	Expression
1		eqid	$⊢ Vtx (G) = Vtx (G)$
2		eqid	$⊢ Edg (G) = Edg (G)$
3	1 2	umgrpredgv	$⊢ (G \in UMGraph \land \{N, N\} \in Edg (G)) \to (N \in Vtx (G) \land N \in Vtx (G))$
4	3	simpld	$⊢ (G \in UMGraph \land \{N, N\} \in Edg (G)) \to N \in Vtx (G)$
5		eqid	$⊢ N = N$
6	2	umgredgne	$⊢ (G \in UMGraph \land \{N, N\} \in Edg (G)) \to N \neq N$
7		eqneqall	$⊢ N = N \to (N \neq N \to \neg N \in Vtx (G))$
8	5 6 7	mpsyl	$⊢ (G \in UMGraph \land \{N, N\} \in Edg (G)) \to \neg N \in Vtx (G)$
9	4 8	pm2.65da	$⊢ G \in UMGraph \to \neg \{N, N\} \in Edg (G)$
10		df-nel	$⊢ \{N, N\} \notin Edg (G) \leftrightarrow \neg \{N, N\} \in Edg (G)$
11	9 10	sylibr	$⊢ G \in UMGraph \to \{N, N\} \notin Edg (G)$

Metamath Proof Explorer