Theorem wkslem1

Description: Lemma 1 for walks to substitute the index of the condition for vertices and edges in a walk. (Contributed by AV, 23-Apr-2021)

	Ref	Expression
Assertion	wkslem1	⊢ ( 𝐴 = 𝐵 → ( if- ( ( 𝑃 ‘ 𝐴 ) = ( 𝑃 ‘ ( 𝐴 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝐴 ) ) = { ( 𝑃 ‘ 𝐴 ) } , { ( 𝑃 ‘ 𝐴 ) , ( 𝑃 ‘ ( 𝐴 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝐴 ) ) ) ↔ if- ( ( 𝑃 ‘ 𝐵 ) = ( 𝑃 ‘ ( 𝐵 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) = { ( 𝑃 ‘ 𝐵 ) } , { ( 𝑃 ‘ 𝐵 ) , ( 𝑃 ‘ ( 𝐵 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		fveq2	⊢ ( 𝐴 = 𝐵 → ( 𝑃 ‘ 𝐴 ) = ( 𝑃 ‘ 𝐵 ) )
2		fvoveq1	⊢ ( 𝐴 = 𝐵 → ( 𝑃 ‘ ( 𝐴 + 1 ) ) = ( 𝑃 ‘ ( 𝐵 + 1 ) ) )
3	1 2	eqeq12d	⊢ ( 𝐴 = 𝐵 → ( ( 𝑃 ‘ 𝐴 ) = ( 𝑃 ‘ ( 𝐴 + 1 ) ) ↔ ( 𝑃 ‘ 𝐵 ) = ( 𝑃 ‘ ( 𝐵 + 1 ) ) ) )
4		2fveq3	⊢ ( 𝐴 = 𝐵 → ( 𝐼 ‘ ( 𝐹 ‘ 𝐴 ) ) = ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) )
5	1	sneqd	⊢ ( 𝐴 = 𝐵 → { ( 𝑃 ‘ 𝐴 ) } = { ( 𝑃 ‘ 𝐵 ) } )
6	4 5	eqeq12d	⊢ ( 𝐴 = 𝐵 → ( ( 𝐼 ‘ ( 𝐹 ‘ 𝐴 ) ) = { ( 𝑃 ‘ 𝐴 ) } ↔ ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) = { ( 𝑃 ‘ 𝐵 ) } ) )
7	1 2	preq12d	⊢ ( 𝐴 = 𝐵 → { ( 𝑃 ‘ 𝐴 ) , ( 𝑃 ‘ ( 𝐴 + 1 ) ) } = { ( 𝑃 ‘ 𝐵 ) , ( 𝑃 ‘ ( 𝐵 + 1 ) ) } )
8	7 4	sseq12d	⊢ ( 𝐴 = 𝐵 → ( { ( 𝑃 ‘ 𝐴 ) , ( 𝑃 ‘ ( 𝐴 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝐴 ) ) ↔ { ( 𝑃 ‘ 𝐵 ) , ( 𝑃 ‘ ( 𝐵 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) ) )
9	3 6 8	ifpbi123d	⊢ ( 𝐴 = 𝐵 → ( if- ( ( 𝑃 ‘ 𝐴 ) = ( 𝑃 ‘ ( 𝐴 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝐴 ) ) = { ( 𝑃 ‘ 𝐴 ) } , { ( 𝑃 ‘ 𝐴 ) , ( 𝑃 ‘ ( 𝐴 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝐴 ) ) ) ↔ if- ( ( 𝑃 ‘ 𝐵 ) = ( 𝑃 ‘ ( 𝐵 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) = { ( 𝑃 ‘ 𝐵 ) } , { ( 𝑃 ‘ 𝐵 ) , ( 𝑃 ‘ ( 𝐵 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) )