Theorem wkslem2

Description: Lemma 2 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	wkslem2	⊢ ( ( 𝐴 = 𝐵 ∧ ( 𝐴 + 1 ) = 𝐶 ) → ( if- ( ( 𝑃 ‘ 𝐴 ) = ( 𝑃 ‘ ( 𝐴 + 1 ) ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝐴 ) ) = { ( 𝑃 ‘ 𝐴 ) } , { ( 𝑃 ‘ 𝐴 ) , ( 𝑃 ‘ ( 𝐴 + 1 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝐴 ) ) ) ↔ if- ( ( 𝑃 ‘ 𝐵 ) = ( 𝑃 ‘ 𝐶 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) = { ( 𝑃 ‘ 𝐵 ) } , { ( 𝑃 ‘ 𝐵 ) , ( 𝑃 ‘ 𝐶 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) )

Proof

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