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