umgrnloopv

Description: In a multigraph, there is no loop, i.e. no edge connecting a vertex with itself. (Contributed by Alexander van der Vekens, 26-Jan-2018) (Revised by AV, 11-Dec-2020)

		Ref	Expression
	Hypothesis	umgrnloopv.e	$⊢ E = iEdg (G)$
	Assertion	umgrnloopv	$⊢ (G \in UMGraph \land M \in W) \to (E (X) = \{M, N\} \to M \neq N)$

Proof

Step	Hyp	Ref	Expression
1		umgrnloopv.e	$⊢ E = iEdg (G)$
2		prnzg	$⊢ M \in W \to \{M, N\} \neq \emptyset$
3	2	adantl	$⊢ (E (X) = \{M, N\} \land M \in W) \to \{M, N\} \neq \emptyset$
4		neeq1	$⊢ E (X) = \{M, N\} \to (E (X) \neq \emptyset \leftrightarrow \{M, N\} \neq \emptyset)$
5	4	adantr	$⊢ (E (X) = \{M, N\} \land M \in W) \to (E (X) \neq \emptyset \leftrightarrow \{M, N\} \neq \emptyset)$
6	3 5	mpbird	$⊢ (E (X) = \{M, N\} \land M \in W) \to E (X) \neq \emptyset$
7		fvfundmfvn0	$⊢ E (X) \neq \emptyset \to (X \in dom E \land Fun ({E ↾}_{\{X\}}))$
8	6 7	syl	$⊢ (E (X) = \{M, N\} \land M \in W) \to (X \in dom E \land Fun ({E ↾}_{\{X\}}))$
9		eqid	$⊢ Vtx (G) = Vtx (G)$
10	9 1	umgredg2	$⊢ (G \in UMGraph \land X \in dom E) \to \|E (X)\| = 2$
11		fveqeq2	$⊢ E (X) = \{M, N\} \to (\|E (X)\| = 2 \leftrightarrow \|\{M, N\}\| = 2)$
12		eqid	$⊢ \{M, N\} = \{M, N\}$
13	12	hashprdifel	$⊢ \|\{M, N\}\| = 2 \to (M \in \{M, N\} \land N \in \{M, N\} \land M \neq N)$
14	13	simp3d	$⊢ \|\{M, N\}\| = 2 \to M \neq N$
15	11 14	syl6bi	$⊢ E (X) = \{M, N\} \to (\|E (X)\| = 2 \to M \neq N)$
16	15	adantr	$⊢ (E (X) = \{M, N\} \land M \in W) \to (\|E (X)\| = 2 \to M \neq N)$
17	10 16	syl5com	$⊢ (G \in UMGraph \land X \in dom E) \to ((E (X) = \{M, N\} \land M \in W) \to M \neq N)$
18	17	expcom	$⊢ X \in dom E \to (G \in UMGraph \to ((E (X) = \{M, N\} \land M \in W) \to M \neq N))$
19	18	com23	$⊢ X \in dom E \to ((E (X) = \{M, N\} \land M \in W) \to (G \in UMGraph \to M \neq N))$
20	19	adantr	$⊢ (X \in dom E \land Fun ({E ↾}_{\{X\}})) \to ((E (X) = \{M, N\} \land M \in W) \to (G \in UMGraph \to M \neq N))$
21	8 20	mpcom	$⊢ (E (X) = \{M, N\} \land M \in W) \to (G \in UMGraph \to M \neq N)$
22	21	ex	$⊢ E (X) = \{M, N\} \to (M \in W \to (G \in UMGraph \to M \neq N))$
23	22	com13	$⊢ G \in UMGraph \to (M \in W \to (E (X) = \{M, N\} \to M \neq N))$
24	23	imp	$⊢ (G \in UMGraph \land M \in W) \to (E (X) = \{M, N\} \to M \neq N)$

Metamath Proof Explorer

Theorem umgrnloopv

Proof