umgr2edg1

Description: If a vertex is adjacent to two different vertices in a multigraph, there is not only one edge starting at this vertex. (Contributed by Alexander van der Vekens, 10-Dec-2017) (Revised by AV, 8-Jun-2021)

	Ref	Expression
Hypotheses	usgrf1oedg.i	$⊢ I = iEdg (G)$
	usgrf1oedg.e	$⊢ E = Edg (G)$
Assertion	umgr2edg1	$⊢ ((G \in UMGraph \land A \neq B) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to \neg \exists! x \in dom I N \in I (x)$

Proof

Step	Hyp	Ref	Expression
1		usgrf1oedg.i	$⊢ I = iEdg (G)$
2		usgrf1oedg.e	$⊢ E = Edg (G)$
3	1 2	umgr2edg	$⊢ ((G \in UMGraph \land A \neq B) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to \exists x \in dom I \exists y \in dom I (x \neq y \land N \in I (x) \land N \in I (y))$
4		3anrot	$⊢ (x \neq y \land N \in I (x) \land N \in I (y)) \leftrightarrow (N \in I (x) \land N \in I (y) \land x \neq y)$
5		df-ne	$⊢ x \neq y \leftrightarrow \neg x = y$
6	5	3anbi3i	$⊢ (N \in I (x) \land N \in I (y) \land x \neq y) \leftrightarrow (N \in I (x) \land N \in I (y) \land \neg x = y)$
7	4 6	bitri	$⊢ (x \neq y \land N \in I (x) \land N \in I (y)) \leftrightarrow (N \in I (x) \land N \in I (y) \land \neg x = y)$
8		df-3an	$⊢ (N \in I (x) \land N \in I (y) \land \neg x = y) \leftrightarrow ((N \in I (x) \land N \in I (y)) \land \neg x = y)$
9	7 8	bitri	$⊢ (x \neq y \land N \in I (x) \land N \in I (y)) \leftrightarrow ((N \in I (x) \land N \in I (y)) \land \neg x = y)$
10	9	2rexbii	$⊢ \exists x \in dom I \exists y \in dom I (x \neq y \land N \in I (x) \land N \in I (y)) \leftrightarrow \exists x \in dom I \exists y \in dom I ((N \in I (x) \land N \in I (y)) \land \neg x = y)$
11	3 10	sylib	$⊢ ((G \in UMGraph \land A \neq B) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to \exists x \in dom I \exists y \in dom I ((N \in I (x) \land N \in I (y)) \land \neg x = y)$
12		rexanali	$⊢ \exists y \in dom I ((N \in I (x) \land N \in I (y)) \land \neg x = y) \leftrightarrow \neg \forall y \in dom I ((N \in I (x) \land N \in I (y)) \to x = y)$
13	12	rexbii	$⊢ \exists x \in dom I \exists y \in dom I ((N \in I (x) \land N \in I (y)) \land \neg x = y) \leftrightarrow \exists x \in dom I \neg \forall y \in dom I ((N \in I (x) \land N \in I (y)) \to x = y)$
14		rexnal	$⊢ \exists x \in dom I \neg \forall y \in dom I ((N \in I (x) \land N \in I (y)) \to x = y) \leftrightarrow \neg \forall x \in dom I \forall y \in dom I ((N \in I (x) \land N \in I (y)) \to x = y)$
15	13 14	bitri	$⊢ \exists x \in dom I \exists y \in dom I ((N \in I (x) \land N \in I (y)) \land \neg x = y) \leftrightarrow \neg \forall x \in dom I \forall y \in dom I ((N \in I (x) \land N \in I (y)) \to x = y)$
16	11 15	sylib	$⊢ ((G \in UMGraph \land A \neq B) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to \neg \forall x \in dom I \forall y \in dom I ((N \in I (x) \land N \in I (y)) \to x = y)$
17	16	intnand	$⊢ ((G \in UMGraph \land A \neq B) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to \neg (\exists x \in dom I N \in I (x) \land \forall x \in dom I \forall y \in dom I ((N \in I (x) \land N \in I (y)) \to x = y))$
18		fveq2	$⊢ x = y \to I (x) = I (y)$
19	18	eleq2d	$⊢ x = y \to (N \in I (x) \leftrightarrow N \in I (y))$
20	19	reu4	$⊢ \exists! x \in dom I N \in I (x) \leftrightarrow (\exists x \in dom I N \in I (x) \land \forall x \in dom I \forall y \in dom I ((N \in I (x) \land N \in I (y)) \to x = y))$
21	17 20	sylnibr	$⊢ ((G \in UMGraph \land A \neq B) \land (\{N, A\} \in E \land \{B, N\} \in E)) \to \neg \exists! x \in dom I N \in I (x)$

Metamath Proof Explorer

Theorem umgr2edg1

Proof