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	⊢ 𝐼 = ⟨“ { 𝑋 , 𝑌 } ”⟩
	wlk2v2e.f	⊢ 𝐹 = ⟨“ 0 0 ”⟩
	wlk2v2e.x	⊢ 𝑋 ∈ V
	wlk2v2e.y	⊢ 𝑌 ∈ V
	wlk2v2e.p	⊢ 𝑃 = ⟨“ 𝑋 𝑌 𝑋 ”⟩
	wlk2v2e.g	⊢ 𝐺 = ⟨ { 𝑋 , 𝑌 } , 𝐼 ⟩
Assertion	ntrl2v2e	⊢ ¬ 𝐹 ( Trails ‘ 𝐺 ) 𝑃

Proof

Step	Hyp	Ref	Expression
1		wlk2v2e.i	⊢ 𝐼 = ⟨“ { 𝑋 , 𝑌 } ”⟩
2		wlk2v2e.f	⊢ 𝐹 = ⟨“ 0 0 ”⟩
3		wlk2v2e.x	⊢ 𝑋 ∈ V
4		wlk2v2e.y	⊢ 𝑌 ∈ V
5		wlk2v2e.p	⊢ 𝑃 = ⟨“ 𝑋 𝑌 𝑋 ”⟩
6		wlk2v2e.g	⊢ 𝐺 = ⟨ { 𝑋 , 𝑌 } , 𝐼 ⟩
7		0z	⊢ 0 ∈ ℤ
8		1z	⊢ 1 ∈ ℤ
9	7 8 7	3pm3.2i	⊢ ( 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 0 ∈ ℤ )
10		0ne1	⊢ 0 ≠ 1
11		s2prop	⊢ ( ( 0 ∈ ℤ ∧ 0 ∈ ℤ ) → ⟨“ 0 0 ”⟩ = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } )
12	7 7 11	mp2an	⊢ ⟨“ 0 0 ”⟩ = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
13	2 12	eqtri	⊢ 𝐹 = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
14	13	fpropnf1	⊢ ( ( ( 0 ∈ ℤ ∧ 1 ∈ ℤ ∧ 0 ∈ ℤ ) ∧ 0 ≠ 1 ) → ( Fun 𝐹 ∧ ¬ Fun ^◡ 𝐹 ) )
15	9 10 14	mp2an	⊢ ( Fun 𝐹 ∧ ¬ Fun ^◡ 𝐹 )
16	15	simpri	⊢ ¬ Fun ^◡ 𝐹
17	16	intnan	⊢ ¬ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ^◡ 𝐹 )
18		istrl	⊢ ( 𝐹 ( Trails ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ∧ Fun ^◡ 𝐹 ) )
19	17 18	mtbir	⊢ ¬ 𝐹 ( Trails ‘ 𝐺 ) 𝑃

Metamath Proof Explorer

Theorem ntrl2v2e

Proof