Metamath Proof Explorer

Theorem 3wlkdlem6

Description: Lemma 6 for 3wlkd . (Contributed 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 3wlkdlem6 
|- ( ph -> ( A e. ( I ` J ) /\ B e. ( I ` K ) /\ C e. ( I ` 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 3wlkdlem3 
 |-  ( ph -> ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) )
7 preq12 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> { ( P ` 0 ) , ( P ` 1 ) } = { A , B } )
8 7 sseq1d 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` J ) <-> { A , B } C_ ( I ` J ) ) )
9 8 adantr 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` J ) <-> { A , B } C_ ( I ` J ) ) )
10 preq12 
 |-  ( ( ( P ` 1 ) = B /\ ( P ` 2 ) = C ) -> { ( P ` 1 ) , ( P ` 2 ) } = { B , C } )
11 10 ad2ant2lr 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> { ( P ` 1 ) , ( P ` 2 ) } = { B , C } )
12 11 sseq1d 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` K ) <-> { B , C } C_ ( I ` K ) ) )
13 preq12 
 |-  ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> { ( P ` 2 ) , ( P ` 3 ) } = { C , D } )
14 13 sseq1d 
 |-  ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> ( { ( P ` 2 ) , ( P ` 3 ) } C_ ( I ` L ) <-> { C , D } C_ ( I ` L ) ) )
15 14 adantl 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( { ( P ` 2 ) , ( P ` 3 ) } C_ ( I ` L ) <-> { C , D } C_ ( I ` L ) ) )
16 9 12 15 3anbi123d 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` J ) /\ { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` K ) /\ { ( P ` 2 ) , ( P ` 3 ) } C_ ( I ` L ) ) <-> ( { A , B } C_ ( I ` J ) /\ { B , C } C_ ( I ` K ) /\ { C , D } C_ ( I ` L ) ) ) )
17 5 16 syl5ibrcom 
 |-  ( ph -> ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` J ) /\ { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` K ) /\ { ( P ` 2 ) , ( P ` 3 ) } C_ ( I ` L ) ) ) )
18 6 17 mpd 
 |-  ( ph -> ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` J ) /\ { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` K ) /\ { ( P ` 2 ) , ( P ` 3 ) } C_ ( I ` L ) ) )
19 fvex 
 |-  ( P ` 0 ) e. _V
20 fvex 
 |-  ( P ` 1 ) e. _V
21 19 20 prss 
 |-  ( ( ( P ` 0 ) e. ( I ` J ) /\ ( P ` 1 ) e. ( I ` J ) ) <-> { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` J ) )
22 simpl 
 |-  ( ( ( P ` 0 ) e. ( I ` J ) /\ ( P ` 1 ) e. ( I ` J ) ) -> ( P ` 0 ) e. ( I ` J ) )
23 21 22 sylbir 
 |-  ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` J ) -> ( P ` 0 ) e. ( I ` J ) )
24 fvex 
 |-  ( P ` 2 ) e. _V
25 20 24 prss 
 |-  ( ( ( P ` 1 ) e. ( I ` K ) /\ ( P ` 2 ) e. ( I ` K ) ) <-> { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` K ) )
26 simpl 
 |-  ( ( ( P ` 1 ) e. ( I ` K ) /\ ( P ` 2 ) e. ( I ` K ) ) -> ( P ` 1 ) e. ( I ` K ) )
27 25 26 sylbir 
 |-  ( { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` K ) -> ( P ` 1 ) e. ( I ` K ) )
28 fvex 
 |-  ( P ` 3 ) e. _V
29 24 28 prss 
 |-  ( ( ( P ` 2 ) e. ( I ` L ) /\ ( P ` 3 ) e. ( I ` L ) ) <-> { ( P ` 2 ) , ( P ` 3 ) } C_ ( I ` L ) )
30 simpl 
 |-  ( ( ( P ` 2 ) e. ( I ` L ) /\ ( P ` 3 ) e. ( I ` L ) ) -> ( P ` 2 ) e. ( I ` L ) )
31 29 30 sylbir 
 |-  ( { ( P ` 2 ) , ( P ` 3 ) } C_ ( I ` L ) -> ( P ` 2 ) e. ( I ` L ) )
32 23 27 31 3anim123i 
 |-  ( ( { ( P ` 0 ) , ( P ` 1 ) } C_ ( I ` J ) /\ { ( P ` 1 ) , ( P ` 2 ) } C_ ( I ` K ) /\ { ( P ` 2 ) , ( P ` 3 ) } C_ ( I ` L ) ) -> ( ( P ` 0 ) e. ( I ` J ) /\ ( P ` 1 ) e. ( I ` K ) /\ ( P ` 2 ) e. ( I ` L ) ) )
33 18 32 syl 
 |-  ( ph -> ( ( P ` 0 ) e. ( I ` J ) /\ ( P ` 1 ) e. ( I ` K ) /\ ( P ` 2 ) e. ( I ` L ) ) )
34 eleq1 
 |-  ( ( P ` 0 ) = A -> ( ( P ` 0 ) e. ( I ` J ) <-> A e. ( I ` J ) ) )
35 34 adantr 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( ( P ` 0 ) e. ( I ` J ) <-> A e. ( I ` J ) ) )
36 35 adantr 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( P ` 0 ) e. ( I ` J ) <-> A e. ( I ` J ) ) )
37 eleq1 
 |-  ( ( P ` 1 ) = B -> ( ( P ` 1 ) e. ( I ` K ) <-> B e. ( I ` K ) ) )
38 37 adantl 
 |-  ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) -> ( ( P ` 1 ) e. ( I ` K ) <-> B e. ( I ` K ) ) )
39 38 adantr 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( P ` 1 ) e. ( I ` K ) <-> B e. ( I ` K ) ) )
40 eleq1 
 |-  ( ( P ` 2 ) = C -> ( ( P ` 2 ) e. ( I ` L ) <-> C e. ( I ` L ) ) )
41 40 adantr 
 |-  ( ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) -> ( ( P ` 2 ) e. ( I ` L ) <-> C e. ( I ` L ) ) )
42 41 adantl 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( P ` 2 ) e. ( I ` L ) <-> C e. ( I ` L ) ) )
43 36 39 42 3anbi123d 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( ( P ` 0 ) e. ( I ` J ) /\ ( P ` 1 ) e. ( I ` K ) /\ ( P ` 2 ) e. ( I ` L ) ) <-> ( A e. ( I ` J ) /\ B e. ( I ` K ) /\ C e. ( I ` L ) ) ) )
44 43 bicomd 
 |-  ( ( ( ( P ` 0 ) = A /\ ( P ` 1 ) = B ) /\ ( ( P ` 2 ) = C /\ ( P ` 3 ) = D ) ) -> ( ( A e. ( I ` J ) /\ B e. ( I ` K ) /\ C e. ( I ` L ) ) <-> ( ( P ` 0 ) e. ( I ` J ) /\ ( P ` 1 ) e. ( I ` K ) /\ ( P ` 2 ) e. ( I ` L ) ) ) )
45 6 44 syl 
 |-  ( ph -> ( ( A e. ( I ` J ) /\ B e. ( I ` K ) /\ C e. ( I ` L ) ) <-> ( ( P ` 0 ) e. ( I ` J ) /\ ( P ` 1 ) e. ( I ` K ) /\ ( P ` 2 ) e. ( I ` L ) ) ) )
46 33 45 mpbird 
 |-  ( ph -> ( A e. ( I ` J ) /\ B e. ( I ` K ) /\ C e. ( I ` L ) ) )