umgrnloop0

Description: A multigraph has no loops. (Contributed by Alexander van der Vekens, 6-Dec-2017) (Revised by AV, 11-Dec-2020)

		Ref	Expression
	Hypothesis	umgrnloopv.e	$⊢ E = iEdg (G)$
	Assertion	umgrnloop0	$⊢ G \in UMGraph \to \{x \in dom E \| E (x) = \{U\}\} = \emptyset$

Step	Hyp	Ref	Expression
1		umgrnloopv.e	$⊢ E = iEdg (G)$
2		neirr	$⊢ \neg U \neq U$
3	1	umgrnloop	$⊢ G \in UMGraph \to (\exists x \in dom E E (x) = \{U, U\} \to U \neq U)$
4	2 3	mtoi	$⊢ G \in UMGraph \to \neg \exists x \in dom E E (x) = \{U, U\}$
5		simpr	$⊢ (G \in UMGraph \land E (x) = \{U\}) \to E (x) = \{U\}$
6		dfsn2	$⊢ \{U\} = \{U, U\}$
7	5 6	eqtrdi	$⊢ (G \in UMGraph \land E (x) = \{U\}) \to E (x) = \{U, U\}$
8	7	ex	$⊢ G \in UMGraph \to (E (x) = \{U\} \to E (x) = \{U, U\})$
9	8	reximdv	$⊢ G \in UMGraph \to (\exists x \in dom E E (x) = \{U\} \to \exists x \in dom E E (x) = \{U, U\})$
10	4 9	mtod	$⊢ G \in UMGraph \to \neg \exists x \in dom E E (x) = \{U\}$
11		ralnex	$⊢ \forall x \in dom E \neg E (x) = \{U\} \leftrightarrow \neg \exists x \in dom E E (x) = \{U\}$
12	10 11	sylibr	$⊢ G \in UMGraph \to \forall x \in dom E \neg E (x) = \{U\}$
13		rabeq0	$⊢ \{x \in dom E \| E (x) = \{U\}\} = \emptyset \leftrightarrow \forall x \in dom E \neg E (x) = \{U\}$
14	12 13	sylibr	$⊢ G \in UMGraph \to \{x \in dom E \| E (x) = \{U\}\} = \emptyset$

Metamath Proof Explorer