Theorem 2wlkdlem6 26827

Description: Lemma 6 for 2wlkd 26832. (Contributed by AV, 23-Jan-2021.)

Hypotheses

Ref	Expression
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

Ref	Expression
2wlkdlem6	|- ( ph -> ( B e. ( I ` J ) /\ B e. ( I ` K ) ) )

Proof of Theorem 2wlkdlem6

Step	Hyp	Ref	Expression
1		2wlkd.e	. 2 |- ( ph -> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) )
2		prcom 4267	. . . . . . . . 9 |- { A , B } = { B , A }
3	2	sseq1i 3629	. . . . . . . 8 |- ( { A , B } C_ ( I ` J ) <-> { B , A } C_ ( I ` J ) )
4	3	biimpi 206	. . . . . . 7 |- ( { A , B } C_ ( I ` J ) -> { B , A } C_ ( I ` J ) )
5	4	adantl 482	. . . . . 6 |- ( ( ph /\ { A , B } C_ ( I ` J ) ) -> { B , A } C_ ( I ` J ) )
6		2wlkd.s	. . . . . . . 8 |- ( ph -> ( A e. V /\ B e. V /\ C e. V ) )
7	6	simp2d 1074	. . . . . . 7 |- ( ph -> B e. V )
8	6	simp1d 1073	. . . . . . . 8 |- ( ph -> A e. V )
9	8	adantr 481	. . . . . . 7 |- ( ( ph /\ { A , B } C_ ( I ` J ) ) -> A e. V )
10		prssg 4350	. . . . . . 7 |- ( ( B e. V /\ A e. V ) -> ( ( B e. ( I ` J ) /\ A e. ( I ` J ) ) <-> { B , A } C_ ( I ` J ) ) )
11	7, 9, 10	syl2an2r 876	. . . . . 6 |- ( ( ph /\ { A , B } C_ ( I ` J ) ) -> ( ( B e. ( I ` J ) /\ A e. ( I ` J ) ) <-> { B , A } C_ ( I ` J ) ) )
12	5, 11	mpbird 247	. . . . 5 |- ( ( ph /\ { A , B } C_ ( I ` J ) ) -> ( B e. ( I ` J ) /\ A e. ( I ` J ) ) )
13	12	simpld 475	. . . 4 |- ( ( ph /\ { A , B } C_ ( I ` J ) ) -> B e. ( I ` J ) )
14	13	ex 450	. . 3 |- ( ph -> ( { A , B } C_ ( I ` J ) -> B e. ( I ` J ) ) )
15		simpr 477	. . . . . 6 |- ( ( ph /\ { B , C } C_ ( I ` K ) ) -> { B , C } C_ ( I ` K ) )
16	6	simp3d 1075	. . . . . . . 8 |- ( ph -> C e. V )
17	16	adantr 481	. . . . . . 7 |- ( ( ph /\ { B , C } C_ ( I ` K ) ) -> C e. V )
18		prssg 4350	. . . . . . 7 |- ( ( B e. V /\ C e. V ) -> ( ( B e. ( I ` K ) /\ C e. ( I ` K ) ) <-> { B , C } C_ ( I ` K ) ) )
19	7, 17, 18	syl2an2r 876	. . . . . 6 |- ( ( ph /\ { B , C } C_ ( I ` K ) ) -> ( ( B e. ( I ` K ) /\ C e. ( I ` K ) ) <-> { B , C } C_ ( I ` K ) ) )
20	15, 19	mpbird 247	. . . . 5 |- ( ( ph /\ { B , C } C_ ( I ` K ) ) -> ( B e. ( I ` K ) /\ C e. ( I ` K ) ) )
21	20	simpld 475	. . . 4 |- ( ( ph /\ { B , C } C_ ( I ` K ) ) -> B e. ( I ` K ) )
22	21	ex 450	. . 3 |- ( ph -> ( { B , C } C_ ( I ` K ) -> B e. ( I ` K ) ) )
23	14, 22	anim12d 586	. 2 |- ( ph -> ( ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) ) -> ( B e. ( I ` J ) /\ B e. ( I ` K ) ) ) )
24	1, 23	mpd 15	1 |- ( ph -> ( B e. ( I ` J ) /\ B e. ( I ` K ) ) )

Syntax hints:   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   C_ wss 3574   {cpr 4179   ` cfv 5888   <"cs2 13586   <"cs3 13587

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588  df-sn 4178  df-pr 4180

This theorem is referenced by:  2wlkdlem7  26828