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

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( A = B -> ( P ` A ) = ( P ` B ) )
2 1 adantr 
 |-  ( ( A = B /\ ( A + 1 ) = C ) -> ( P ` A ) = ( P ` B ) )
3 fveq2 
 |-  ( ( A + 1 ) = C -> ( P ` ( A + 1 ) ) = ( P ` C ) )
4 3 adantl 
 |-  ( ( A = B /\ ( A + 1 ) = C ) -> ( P ` ( A + 1 ) ) = ( P ` C ) )
5 2 4 eqeq12d 
 |-  ( ( A = B /\ ( A + 1 ) = C ) -> ( ( P ` A ) = ( P ` ( A + 1 ) ) <-> ( P ` B ) = ( P ` C ) ) )
6 2fveq3 
 |-  ( A = B -> ( I ` ( F ` A ) ) = ( I ` ( F ` B ) ) )
7 1 sneqd 
 |-  ( A = B -> { ( P ` A ) } = { ( P ` B ) } )
8 6 7 eqeq12d 
 |-  ( A = B -> ( ( I ` ( F ` A ) ) = { ( P ` A ) } <-> ( I ` ( F ` B ) ) = { ( P ` B ) } ) )
9 8 adantr 
 |-  ( ( A = B /\ ( A + 1 ) = C ) -> ( ( I ` ( F ` A ) ) = { ( P ` A ) } <-> ( I ` ( F ` B ) ) = { ( P ` B ) } ) )
10 2 4 preq12d 
 |-  ( ( A = B /\ ( A + 1 ) = C ) -> { ( P ` A ) , ( P ` ( A + 1 ) ) } = { ( P ` B ) , ( P ` C ) } )
11 6 adantr 
 |-  ( ( A = B /\ ( A + 1 ) = C ) -> ( I ` ( F ` A ) ) = ( I ` ( F ` B ) ) )
12 10 11 sseq12d 
 |-  ( ( A = B /\ ( A + 1 ) = C ) -> ( { ( P ` A ) , ( P ` ( A + 1 ) ) } C_ ( I ` ( F ` A ) ) <-> { ( P ` B ) , ( P ` C ) } C_ ( I ` ( F ` B ) ) ) )
13 5 9 12 ifpbi123d 
 |-  ( ( A = B /\ ( A + 1 ) = C ) -> ( if- ( ( P ` A ) = ( P ` ( A + 1 ) ) , ( I ` ( F ` A ) ) = { ( P ` A ) } , { ( P ` A ) , ( P ` ( A + 1 ) ) } C_ ( I ` ( F ` A ) ) ) <-> if- ( ( P ` B ) = ( P ` C ) , ( I ` ( F ` B ) ) = { ( P ` B ) } , { ( P ` B ) , ( P ` C ) } C_ ( I ` ( F ` B ) ) ) ) )