ntrl2v2e

Description: A walk which is not a trail: In a graph with two vertices and one edge connecting these two vertices, to go from one vertex to the other and back to the first vertex via the same/only edge is a walk, see wlk2v2e , but not a trail. Notice that G is a simple graph (without loops) only if X =/= Y . (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 8-Jan-2021) (Proof shortened by AV, 30-Oct-2021)

	Ref	Expression
Hypotheses	wlk2v2e.i	$⊢ I = ⟨“ \{X, Y\} ”⟩$
	wlk2v2e.f	$⊢ F = ⟨“ 00 ”⟩$
	wlk2v2e.x	$⊢ X \in V$
	wlk2v2e.y	$⊢ Y \in V$
	wlk2v2e.p	$⊢ P = ⟨“ X Y X ”⟩$
	wlk2v2e.g	$⊢ G = ⟨\{X, Y\}, I⟩$
Assertion	ntrl2v2e	$⊢ \neg F Trails (G) P$

Proof

Step	Hyp	Ref	Expression
1		wlk2v2e.i	$⊢ I = ⟨“ \{X, Y\} ”⟩$
2		wlk2v2e.f	$⊢ F = ⟨“ 00 ”⟩$
3		wlk2v2e.x	$⊢ X \in V$
4		wlk2v2e.y	$⊢ Y \in V$
5		wlk2v2e.p	$⊢ P = ⟨“ X Y X ”⟩$
6		wlk2v2e.g	$⊢ G = ⟨\{X, Y\}, I⟩$
7		0z	$⊢ 0 \in ℤ$
8		1z	$⊢ 1 \in ℤ$
9	7 8 7	3pm3.2i	$⊢ (0 \in ℤ \land 1 \in ℤ \land 0 \in ℤ)$
10		0ne1	$⊢ 0 \neq 1$
11		s2prop	$⊢ (0 \in ℤ \land 0 \in ℤ) \to ⟨“ 00 ”⟩ = \{⟨0, 0⟩, ⟨1, 0⟩\}$
12	7 7 11	mp2an	$⊢ ⟨“ 00 ”⟩ = \{⟨0, 0⟩, ⟨1, 0⟩\}$
13	2 12	eqtri	$⊢ F = \{⟨0, 0⟩, ⟨1, 0⟩\}$
14	13	fpropnf1	$⊢ ((0 \in ℤ \land 1 \in ℤ \land 0 \in ℤ) \land 0 \neq 1) \to (Fun F \land \neg Fun F^{-1})$
15	9 10 14	mp2an	$⊢ (Fun F \land \neg Fun F^{-1})$
16	15	simpri	$⊢ \neg Fun F^{-1}$
17	16	intnan	$⊢ \neg (F Walks (G) P \land Fun F^{-1})$
18		istrl	$⊢ F Trails (G) P \leftrightarrow (F Walks (G) P \land Fun F^{-1})$
19	17 18	mtbir	$⊢ \neg F Trails (G) P$

Metamath Proof Explorer

Theorem ntrl2v2e

Proof