Theorem 3wlkdlem8

Description: Lemma 8 for 3wlkd . (Contributed by Alexander van der Vekens, 12-Nov-2017) (Revised 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	3wlkdlem8	|- ( ph -> ( ( F ` 0 ) = J /\ ( F ` 1 ) = K /\ ( F ` 2 ) = L ) )

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	3wlkdlem7	|- ( ph -> ( J e. _V /\ K e. _V /\ L e. _V ) )
7		s3fv0	|- ( J e. _V -> ( <" J K L "> ` 0 ) = J )
8		s3fv1	|- ( K e. _V -> ( <" J K L "> ` 1 ) = K )
9		s3fv2	|- ( L e. _V -> ( <" J K L "> ` 2 ) = L )
10	7 8 9	3anim123i	|- ( ( J e. _V /\ K e. _V /\ L e. _V ) -> ( ( <" J K L "> ` 0 ) = J /\ ( <" J K L "> ` 1 ) = K /\ ( <" J K L "> ` 2 ) = L ) )
11	6 10	syl	|- ( ph -> ( ( <" J K L "> ` 0 ) = J /\ ( <" J K L "> ` 1 ) = K /\ ( <" J K L "> ` 2 ) = L ) )
12	2	fveq1i	|- ( F ` 0 ) = ( <" J K L "> ` 0 )
13	12	eqeq1i	|- ( ( F ` 0 ) = J <-> ( <" J K L "> ` 0 ) = J )
14	2	fveq1i	|- ( F ` 1 ) = ( <" J K L "> ` 1 )
15	14	eqeq1i	|- ( ( F ` 1 ) = K <-> ( <" J K L "> ` 1 ) = K )
16	2	fveq1i	|- ( F ` 2 ) = ( <" J K L "> ` 2 )
17	16	eqeq1i	|- ( ( F ` 2 ) = L <-> ( <" J K L "> ` 2 ) = L )
18	13 15 17	3anbi123i	|- ( ( ( F ` 0 ) = J /\ ( F ` 1 ) = K /\ ( F ` 2 ) = L ) <-> ( ( <" J K L "> ` 0 ) = J /\ ( <" J K L "> ` 1 ) = K /\ ( <" J K L "> ` 2 ) = L ) )
19	11 18	sylibr	|- ( ph -> ( ( F ` 0 ) = J /\ ( F ` 1 ) = K /\ ( F ` 2 ) = L ) )