Theorem 2wlklem

Description: Lemma for theorems for walks of length 2. (Contributed by Alexander van der Vekens, 1-Feb-2018)

	Ref	Expression
Assertion	2wlklem	⊢ ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( 𝐸 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐸 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		c0ex	⊢ 0 ∈ V
2		1ex	⊢ 1 ∈ V
3		2fveq3	⊢ ( 𝑘 = 0 → ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ 0 ) ) )
4		fveq2	⊢ ( 𝑘 = 0 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 0 ) )
5		fv0p1e1	⊢ ( 𝑘 = 0 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 1 ) )
6	4 5	preq12d	⊢ ( 𝑘 = 0 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } )
7	3 6	eqeq12d	⊢ ( 𝑘 = 0 → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( 𝐸 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ) )
8		2fveq3	⊢ ( 𝑘 = 1 → ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = ( 𝐸 ‘ ( 𝐹 ‘ 1 ) ) )
9		fveq2	⊢ ( 𝑘 = 1 → ( 𝑃 ‘ 𝑘 ) = ( 𝑃 ‘ 1 ) )
10		oveq1	⊢ ( 𝑘 = 1 → ( 𝑘 + 1 ) = ( 1 + 1 ) )
11		1p1e2	⊢ ( 1 + 1 ) = 2
12	10 11	eqtrdi	⊢ ( 𝑘 = 1 → ( 𝑘 + 1 ) = 2 )
13	12	fveq2d	⊢ ( 𝑘 = 1 → ( 𝑃 ‘ ( 𝑘 + 1 ) ) = ( 𝑃 ‘ 2 ) )
14	9 13	preq12d	⊢ ( 𝑘 = 1 → { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } )
15	8 14	eqeq12d	⊢ ( 𝑘 = 1 → ( ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( 𝐸 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )
16	1 2 7 15	ralpr	⊢ ( ∀ 𝑘 ∈ { 0 , 1 } ( 𝐸 ‘ ( 𝐹 ‘ 𝑘 ) ) = { ( 𝑃 ‘ 𝑘 ) , ( 𝑃 ‘ ( 𝑘 + 1 ) ) } ↔ ( ( 𝐸 ‘ ( 𝐹 ‘ 0 ) ) = { ( 𝑃 ‘ 0 ) , ( 𝑃 ‘ 1 ) } ∧ ( 𝐸 ‘ ( 𝐹 ‘ 1 ) ) = { ( 𝑃 ‘ 1 ) , ( 𝑃 ‘ 2 ) } ) )