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

Metamath Proof Explorer

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 ) ) } ⊆ ( 𝐼 ‘ ( 𝐹 ‘ 𝐵 ) ) ) ) )