Theorem wlk2v2e

Description: 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. 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)

	Ref	Expression
Hypotheses	wlk2v2e.i	⊢ 𝐼 = ⟨“ { 𝑋 , 𝑌 } ”⟩
	wlk2v2e.f	⊢ 𝐹 = ⟨“ 0 0 ”⟩
	wlk2v2e.x	⊢ 𝑋 ∈ V
	wlk2v2e.y	⊢ 𝑌 ∈ V
	wlk2v2e.p	⊢ 𝑃 = ⟨“ 𝑋 𝑌 𝑋 ”⟩
	wlk2v2e.g	⊢ 𝐺 = ⟨ { 𝑋 , 𝑌 } , 𝐼 ⟩
Assertion	wlk2v2e	⊢ 𝐹 ( Walks ‘ 𝐺 ) 𝑃

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	1	opeq2i	⊢ ⟨ { 𝑋 , 𝑌 } , 𝐼 ⟩ = ⟨ { 𝑋 , 𝑌 } , ⟨“ { 𝑋 , 𝑌 } ”⟩ ⟩
8	6 7	eqtri	⊢ 𝐺 = ⟨ { 𝑋 , 𝑌 } , ⟨“ { 𝑋 , 𝑌 } ”⟩ ⟩
9		uspgr2v1e2w	⊢ ( ( 𝑋 ∈ V ∧ 𝑌 ∈ V ) → ⟨ { 𝑋 , 𝑌 } , ⟨“ { 𝑋 , 𝑌 } ”⟩ ⟩ ∈ USPGraph )
10	3 4 9	mp2an	⊢ ⟨ { 𝑋 , 𝑌 } , ⟨“ { 𝑋 , 𝑌 } ”⟩ ⟩ ∈ USPGraph
11	8 10	eqeltri	⊢ 𝐺 ∈ USPGraph
12		uspgrupgr	⊢ ( 𝐺 ∈ USPGraph → 𝐺 ∈ UPGraph )
13	11 12	ax-mp	⊢ 𝐺 ∈ UPGraph
14	1 2	wlk2v2elem1	⊢ 𝐹 ∈ Word dom 𝐼
15	3	prid1	⊢ 𝑋 ∈ { 𝑋 , 𝑌 }
16	4	prid2	⊢ 𝑌 ∈ { 𝑋 , 𝑌 }
17		s3cl	⊢ ( ( 𝑋 ∈ { 𝑋 , 𝑌 } ∧ 𝑌 ∈ { 𝑋 , 𝑌 } ∧ 𝑋 ∈ { 𝑋 , 𝑌 } ) → ⟨“ 𝑋 𝑌 𝑋 ”⟩ ∈ Word { 𝑋 , 𝑌 } )
18	15 16 15 17	mp3an	⊢ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ∈ Word { 𝑋 , 𝑌 }
19	5 18	eqeltri	⊢ 𝑃 ∈ Word { 𝑋 , 𝑌 }
20		wrdf	⊢ ( 𝑃 ∈ Word { 𝑋 , 𝑌 } → 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ { 𝑋 , 𝑌 } )
21	19 20	ax-mp	⊢ 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ { 𝑋 , 𝑌 }
22	5	fveq2i	⊢ ( ♯ ‘ 𝑃 ) = ( ♯ ‘ ⟨“ 𝑋 𝑌 𝑋 ”⟩ )
23		s3len	⊢ ( ♯ ‘ ⟨“ 𝑋 𝑌 𝑋 ”⟩ ) = 3
24	22 23	eqtr2i	⊢ 3 = ( ♯ ‘ 𝑃 )
25	24	oveq2i	⊢ ( 0 ..^ 3 ) = ( 0 ..^ ( ♯ ‘ 𝑃 ) )
26	25	feq2i	⊢ ( 𝑃 : ( 0 ..^ 3 ) ⟶ { 𝑋 , 𝑌 } ↔ 𝑃 : ( 0 ..^ ( ♯ ‘ 𝑃 ) ) ⟶ { 𝑋 , 𝑌 } )
27	21 26	mpbir	⊢ 𝑃 : ( 0 ..^ 3 ) ⟶ { 𝑋 , 𝑌 }
28	2	fveq2i	⊢ ( ♯ ‘ 𝐹 ) = ( ♯ ‘ ⟨“ 0 0 ”⟩ )
29		s2len	⊢ ( ♯ ‘ ⟨“ 0 0 ”⟩ ) = 2
30	28 29	eqtri	⊢ ( ♯ ‘ 𝐹 ) = 2
31	30	oveq2i	⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ... 2 )
32		3z	⊢ 3 ∈ ℤ
33		fzoval	⊢ ( 3 ∈ ℤ → ( 0 ..^ 3 ) = ( 0 ... ( 3 − 1 ) ) )
34	32 33	ax-mp	⊢ ( 0 ..^ 3 ) = ( 0 ... ( 3 − 1 ) )
35		3m1e2	⊢ ( 3 − 1 ) = 2
36	35	oveq2i	⊢ ( 0 ... ( 3 − 1 ) ) = ( 0 ... 2 )
37	34 36	eqtr2i	⊢ ( 0 ... 2 ) = ( 0 ..^ 3 )
38	31 37	eqtri	⊢ ( 0 ... ( ♯ ‘ 𝐹 ) ) = ( 0 ..^ 3 )
39	38	feq2i	⊢ ( 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ { 𝑋 , 𝑌 } ↔ 𝑃 : ( 0 ..^ 3 ) ⟶ { 𝑋 , 𝑌 } )
40	27 39	mpbir	⊢ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ { 𝑋 , 𝑌 }
41	1 2 3 4 5	wlk2v2elem2	⊢ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) }
42	14 40 41	3pm3.2i	⊢ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ { 𝑋 , 𝑌 } ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
43	6	fveq2i	⊢ ( Vtx ‘ 𝐺 ) = ( Vtx ‘ ⟨ { 𝑋 , 𝑌 } , 𝐼 ⟩ )
44		prex	⊢ { 𝑋 , 𝑌 } ∈ V
45		s1cli	⊢ ⟨“ { 𝑋 , 𝑌 } ”⟩ ∈ Word V
46	1 45	eqeltri	⊢ 𝐼 ∈ Word V
47		opvtxfv	⊢ ( ( { 𝑋 , 𝑌 } ∈ V ∧ 𝐼 ∈ Word V ) → ( Vtx ‘ ⟨ { 𝑋 , 𝑌 } , 𝐼 ⟩ ) = { 𝑋 , 𝑌 } )
48	44 46 47	mp2an	⊢ ( Vtx ‘ ⟨ { 𝑋 , 𝑌 } , 𝐼 ⟩ ) = { 𝑋 , 𝑌 }
49	43 48	eqtr2i	⊢ { 𝑋 , 𝑌 } = ( Vtx ‘ 𝐺 )
50	6	fveq2i	⊢ ( iEdg ‘ 𝐺 ) = ( iEdg ‘ ⟨ { 𝑋 , 𝑌 } , 𝐼 ⟩ )
51		opiedgfv	⊢ ( ( { 𝑋 , 𝑌 } ∈ V ∧ 𝐼 ∈ Word V ) → ( iEdg ‘ ⟨ { 𝑋 , 𝑌 } , 𝐼 ⟩ ) = 𝐼 )
52	44 46 51	mp2an	⊢ ( iEdg ‘ ⟨ { 𝑋 , 𝑌 } , 𝐼 ⟩ ) = 𝐼
53	50 52	eqtr2i	⊢ 𝐼 = ( iEdg ‘ 𝐺 )
54	49 53	upgriswlk	⊢ ( 𝐺 ∈ UPGraph → ( 𝐹 ( Walks ‘ 𝐺 ) 𝑃 ↔ ( 𝐹 ∈ Word dom 𝐼 ∧ 𝑃 : ( 0 ... ( ♯ ‘ 𝐹 ) ) ⟶ { 𝑋 , 𝑌 } ∧ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ) ) )
55	42 54	mpbiri	⊢ ( 𝐺 ∈ UPGraph → 𝐹 ( Walks ‘ 𝐺 ) 𝑃 )
56	13 55	ax-mp	⊢ 𝐹 ( Walks ‘ 𝐺 ) 𝑃