Metamath Proof Explorer

Theorem 3wlkdlem9

Description: Lemma 9 for 3wlkd . (Contributed by AV, 7-Feb-2021)

Ref Expression
Hypotheses 3wlkd.p 
|- P = <" A B C D ">
3wlkd.f 
|- F = <" J K L ">
3wlkd.s 
|- ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )
3wlkd.n 
|- ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )
3wlkd.e 
|- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )
Assertion 3wlkdlem9 
|- ( ph -> ( { A , B } C_ ( I ` ( F ` 0 ) ) /\ { B , C } C_ ( I ` ( F ` 1 ) ) /\ { C , D } C_ ( I ` ( F ` 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 3wlkd.p 
 |-  P = <" A B C D ">
2 3wlkd.f 
 |-  F = <" J K L ">
3 3wlkd.s 
 |-  ( ph -> ( ( A e. V /\ B e. V ) /\ ( C e. V /\ D e. V ) ) )
4 3wlkd.n 
 |-  ( ph -> ( ( A =/= B /\ A =/= C ) /\ ( B =/= C /\ B =/= D ) /\ C =/= D ) )
5 3wlkd.e 
 |-  ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) )
6 1 2 3 4 5 3wlkdlem8 
 |-  ( ph -> ( ( F ` 0 ) = J /\ ( F ` 1 ) = K /\ ( F ` 2 ) = L ) )
7 fveq2 
 |-  ( ( F ` 0 ) = J -> ( I ` ( F ` 0 ) ) = ( I ` J ) )
8 7 sseq2d 
 |-  ( ( F ` 0 ) = J -> ( { A , B } C_ ( I ` ( F ` 0 ) ) <-> { A , B } C_ ( I ` J ) ) )
9 8 3ad2ant1 
 |-  ( ( ( F ` 0 ) = J /\ ( F ` 1 ) = K /\ ( F ` 2 ) = L ) -> ( { A , B } C_ ( I ` ( F ` 0 ) ) <-> { A , B } C_ ( I ` J ) ) )
10 fveq2 
 |-  ( ( F ` 1 ) = K -> ( I ` ( F ` 1 ) ) = ( I ` K ) )
11 10 sseq2d 
 |-  ( ( F ` 1 ) = K -> ( { B , C } C_ ( I ` ( F ` 1 ) ) <-> { B , C } C_ ( I ` K ) ) )
12 11 3ad2ant2 
 |-  ( ( ( F ` 0 ) = J /\ ( F ` 1 ) = K /\ ( F ` 2 ) = L ) -> ( { B , C } C_ ( I ` ( F ` 1 ) ) <-> { B , C } C_ ( I ` K ) ) )
13 fveq2 
 |-  ( ( F ` 2 ) = L -> ( I ` ( F ` 2 ) ) = ( I ` L ) )
14 13 sseq2d 
 |-  ( ( F ` 2 ) = L -> ( { C , D } C_ ( I ` ( F ` 2 ) ) <-> { C , D } C_ ( I ` L ) ) )
15 14 3ad2ant3 
 |-  ( ( ( F ` 0 ) = J /\ ( F ` 1 ) = K /\ ( F ` 2 ) = L ) -> ( { C , D } C_ ( I ` ( F ` 2 ) ) <-> { C , D } C_ ( I ` L ) ) )
16 9 12 15 3anbi123d 
 |-  ( ( ( F ` 0 ) = J /\ ( F ` 1 ) = K /\ ( F ` 2 ) = L ) -> ( ( { A , B } C_ ( I ` ( F ` 0 ) ) /\ { B , C } C_ ( I ` ( F ` 1 ) ) /\ { C , D } C_ ( I ` ( F ` 2 ) ) ) <-> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) ) )
17 6 16 syl 
 |-  ( ph -> ( ( { A , B } C_ ( I ` ( F ` 0 ) ) /\ { B , C } C_ ( I ` ( F ` 1 ) ) /\ { C , D } C_ ( I ` ( F ` 2 ) ) ) <-> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) ) )
18 5 17 mpbird 
 |-  ( ph -> ( { A , B } C_ ( I ` ( F ` 0 ) ) /\ { B , C } C_ ( I ` ( F ` 1 ) ) /\ { C , D } C_ ( I ` ( F ` 2 ) ) ) )