Metamath Proof Explorer

Theorem 2wlkdlem6

Description: Lemma 6 for 2wlkd . (Contributed by AV, 23-Jan-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 2wlkdlem6 
|- ( ph -> ( B e. ( I ` J ) /\ B e. ( I ` K ) ) )

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 prcom 
 |-  { A , B } = { B , A }
7 6 sseq1i 
 |-  ( { A , B } C_ ( I ` J ) <-> { B , A } C_ ( I ` J ) )
8 7 bilani 
 |-  ( ( ph /\ { A , B } C_ ( I ` J ) ) -> { B , A } C_ ( I ` J ) )
9 3 simp2d 
 |-  ( ph -> B e. V )
10 3 simp1d 
 |-  ( ph -> A e. V )
11 10 adantr 
 |-  ( ( ph /\ { A , B } C_ ( I ` J ) ) -> A e. V )
12 prssg 
 |-  ( ( B e. V /\ A e. V ) -> ( ( B e. ( I ` J ) /\ A e. ( I ` J ) ) <-> { B , A } C_ ( I ` J ) ) )
13 9 11 12 syl2an2r 
 |-  ( ( ph /\ { A , B } C_ ( I ` J ) ) -> ( ( B e. ( I ` J ) /\ A e. ( I ` J ) ) <-> { B , A } C_ ( I ` J ) ) )
14 8 13 mpbird 
 |-  ( ( ph /\ { A , B } C_ ( I ` J ) ) -> ( B e. ( I ` J ) /\ A e. ( I ` J ) ) )
15 14 simpld 
 |-  ( ( ph /\ { A , B } C_ ( I ` J ) ) -> B e. ( I ` J ) )
16 15 ex 
 |-  ( ph -> ( { A , B } C_ ( I ` J ) -> B e. ( I ` J ) ) )
17 simpr 
 |-  ( ( ph /\ { B , C } C_ ( I ` K ) ) -> { B , C } C_ ( I ` K ) )
18 3 simp3d 
 |-  ( ph -> C e. V )
19 18 adantr 
 |-  ( ( ph /\ { B , C } C_ ( I ` K ) ) -> C e. V )
20 prssg 
 |-  ( ( B e. V /\ C e. V ) -> ( ( B e. ( I ` K ) /\ C e. ( I ` K ) ) <-> { B , C } C_ ( I ` K ) ) )
21 9 19 20 syl2an2r 
 |-  ( ( ph /\ { B , C } C_ ( I ` K ) ) -> ( ( B e. ( I ` K ) /\ C e. ( I ` K ) ) <-> { B , C } C_ ( I ` K ) ) )
22 17 21 mpbird 
 |-  ( ( ph /\ { B , C } C_ ( I ` K ) ) -> ( B e. ( I ` K ) /\ C e. ( I ` K ) ) )
23 22 simpld 
 |-  ( ( ph /\ { B , C } C_ ( I ` K ) ) -> B e. ( I ` K ) )
24 23 ex 
 |-  ( ph -> ( { B , C } C_ ( I ` K ) -> B e. ( I ` K ) ) )
25 16 24 anim12d 
 |-  ( ph -> ( ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) -> ( B e. ( I ` J ) /\ B e. ( I ` K ) ) ) )
26 5 25 mpd 
 |-  ( ph -> ( B e. ( I ` J ) /\ B e. ( I ` K ) ) )