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 
|- ( A = B -> ( if- ( ( P ` A ) = ( P ` ( A + 1 ) ) , ( I ` ( F ` A ) ) = { ( P ` A ) } , { ( P ` A ) , ( P ` ( A + 1 ) ) } C_ ( I ` ( F ` A ) ) ) <-> if- ( ( P ` B ) = ( P ` ( B + 1 ) ) , ( I ` ( F ` B ) ) = { ( P ` B ) } , { ( P ` B ) , ( P ` ( B + 1 ) ) } C_ ( I ` ( F ` B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = B -> ( P ` A ) = ( P ` B ) )
2 fvoveq1 
 |-  ( A = B -> ( P ` ( A + 1 ) ) = ( P ` ( B + 1 ) ) )
3 1 2 eqeq12d 
 |-  ( A = B -> ( ( P ` A ) = ( P ` ( A + 1 ) ) <-> ( P ` B ) = ( P ` ( B + 1 ) ) ) )
4 2fveq3 
 |-  ( A = B -> ( I ` ( F ` A ) ) = ( I ` ( F ` B ) ) )
5 1 sneqd 
 |-  ( A = B -> { ( P ` A ) } = { ( P ` B ) } )
6 4 5 eqeq12d 
 |-  ( A = B -> ( ( I ` ( F ` A ) ) = { ( P ` A ) } <-> ( I ` ( F ` B ) ) = { ( P ` B ) } ) )
7 1 2 preq12d 
 |-  ( A = B -> { ( P ` A ) , ( P ` ( A + 1 ) ) } = { ( P ` B ) , ( P ` ( B + 1 ) ) } )
8 7 4 sseq12d 
 |-  ( A = B -> ( { ( P ` A ) , ( P ` ( A + 1 ) ) } C_ ( I ` ( F ` A ) ) <-> { ( P ` B ) , ( P ` ( B + 1 ) ) } C_ ( I ` ( F ` B ) ) ) )
9 3 6 8 ifpbi123d 
 |-  ( A = B -> ( if- ( ( P ` A ) = ( P ` ( A + 1 ) ) , ( I ` ( F ` A ) ) = { ( P ` A ) } , { ( P ` A ) , ( P ` ( A + 1 ) ) } C_ ( I ` ( F ` A ) ) ) <-> if- ( ( P ` B ) = ( P ` ( B + 1 ) ) , ( I ` ( F ` B ) ) = { ( P ` B ) } , { ( P ` B ) , ( P ` ( B + 1 ) ) } C_ ( I ` ( F ` B ) ) ) ) )