Theorem 2wlkdlem9

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

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

Proof

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