Theorem wlk2v2elem2

Description: Lemma 2 for wlk2v2e : The values of I after F are edges between two vertices enumerated by P . (Contributed by Alexander van der Vekens, 22-Oct-2017) (Revised by AV, 9-Jan-2021)

	Ref	Expression
Hypotheses	wlk2v2e.i	⊢ 𝐼 = ⟨“ { 𝑋 , 𝑌 } ”⟩
	wlk2v2e.f	⊢ 𝐹 = ⟨“ 0 0 ”⟩
	wlk2v2e.x	⊢ 𝑋 ∈ V
	wlk2v2e.y	⊢ 𝑌 ∈ V
	wlk2v2e.p	⊢ 𝑃 = ⟨“ 𝑋 𝑌 𝑋 ”⟩
Assertion	wlk2v2elem2	⊢ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) }

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	2	fveq1i	⊢ ( 𝐹 ‘ 0 ) = ( ⟨“ 0 0 ”⟩ ‘ 0 )
7		0z	⊢ 0 ∈ ℤ
8		s2fv0	⊢ ( 0 ∈ ℤ → ( ⟨“ 0 0 ”⟩ ‘ 0 ) = 0 )
9	7 8	ax-mp	⊢ ( ⟨“ 0 0 ”⟩ ‘ 0 ) = 0
10	6 9	eqtri	⊢ ( 𝐹 ‘ 0 ) = 0
11	10	fveq2i	⊢ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = ( 𝐼 ‘ 0 )
12	1	fveq1i	⊢ ( 𝐼 ‘ 0 ) = ( ⟨“ { 𝑋 , 𝑌 } ”⟩ ‘ 0 )
13		prex	⊢ { 𝑋 , 𝑌 } ∈ V
14		s1fv	⊢ ( { 𝑋 , 𝑌 } ∈ V → ( ⟨“ { 𝑋 , 𝑌 } ”⟩ ‘ 0 ) = { 𝑋 , 𝑌 } )
15	13 14	ax-mp	⊢ ( ⟨“ { 𝑋 , 𝑌 } ”⟩ ‘ 0 ) = { 𝑋 , 𝑌 }
16	12 15	eqtri	⊢ ( 𝐼 ‘ 0 ) = { 𝑋 , 𝑌 }
17	5	fveq1i	⊢ ( 𝑃 ‘ 0 ) = ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 0 )
18		s3fv0	⊢ ( 𝑋 ∈ V → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 0 ) = 𝑋 )
19	3 18	ax-mp	⊢ ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 0 ) = 𝑋
20	17 19	eqtri	⊢ ( 𝑃 ‘ 0 ) = 𝑋
21	5	fveq1i	⊢ ( 𝑃 ‘ 1 ) = ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 1 )
22		s3fv1	⊢ ( 𝑌 ∈ V → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 1 ) = 𝑌 )
23	4 22	ax-mp	⊢ ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 1 ) = 𝑌
24	21 23	eqtri	⊢ ( 𝑃 ‘ 1 ) = 𝑌
25	20 24	preq12i	⊢ { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } = { 𝑋 , 𝑌 }
26	25	eqcomi	⊢ { 𝑋 , 𝑌 } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) }
27	11 16 26	3eqtri	⊢ ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) }
28	2	fveq1i	⊢ ( 𝐹 ‘ 1 ) = ( ⟨“ 0 0 ”⟩ ‘ 1 )
29		s2fv1	⊢ ( 0 ∈ ℤ → ( ⟨“ 0 0 ”⟩ ‘ 1 ) = 0 )
30	7 29	ax-mp	⊢ ( ⟨“ 0 0 ”⟩ ‘ 1 ) = 0
31	28 30	eqtri	⊢ ( 𝐹 ‘ 1 ) = 0
32	31	fveq2i	⊢ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = ( 𝐼 ‘ 0 )
33		prcom	⊢ { 𝑋 , 𝑌 } = { 𝑌 , 𝑋 }
34	5	fveq1i	⊢ ( 𝑃 ‘ 2 ) = ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 2 )
35		s3fv2	⊢ ( 𝑋 ∈ V → ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 2 ) = 𝑋 )
36	3 35	ax-mp	⊢ ( ⟨“ 𝑋 𝑌 𝑋 ”⟩ ‘ 2 ) = 𝑋
37	34 36	eqtri	⊢ ( 𝑃 ‘ 2 ) = 𝑋
38	24 37	preq12i	⊢ { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } = { 𝑌 , 𝑋 }
39	38	eqcomi	⊢ { 𝑌 , 𝑋 } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) }
40	33 39	eqtri	⊢ { 𝑋 , 𝑌 } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) }
41	32 16 40	3eqtri	⊢ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) }
42		2wlklem	⊢ ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( 𝐼 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐼 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
43	27 41 42	mpbir2an	⊢ ∀ 𝑘 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) }
44	5 2	2wlkdlem2	⊢ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) = { 0 , 1 }
45	44	raleqi	⊢ ( ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ∀ 𝑘 ∈ { 0 , 1 } ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } )
46	43 45	mpbir	⊢ ∀ 𝑘 ∈ ( 0 ..^ ( ♯ ‘ 𝐹 ) ) ( 𝐼 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) }