This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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- ( ( 𝑃 ‘ 𝐵 ) = ( 𝑃 ‘ 𝐶 ) , ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) = { ( 𝑃 ‘ 𝐵 ) } , { ( 𝑃 ‘ 𝐵 ) , ( 𝑃 ‘ 𝐶 ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) )