Metamath Proof Explorer


Theorem lhpexle3

Description: There exists atom under a co-atom different from any three other elements. (Contributed by NM, 24-Jul-2013)

Ref Expression
Hypotheses lhpex1.l ˙=K
lhpex1.a A=AtomsK
lhpex1.h H=LHypK
Assertion lhpexle3 KHLWHpAp˙WpXpYpZ

Proof

Step Hyp Ref Expression
1 lhpex1.l ˙=K
2 lhpex1.a A=AtomsK
3 lhpex1.h H=LHypK
4 1 2 3 lhpexle2 KHLWHpAp˙WpXpY
5 3anass p˙WpXpYp˙WpXpY
6 5 rexbii pAp˙WpXpYpAp˙WpXpY
7 4 6 sylib KHLWHpAp˙WpXpY
8 1 2 3 lhpexle2 KHLWHpAp˙WpXpZ
9 8 adantr KHLWHZAZ˙WpAp˙WpXpZ
10 3anass p˙WpXpZp˙WpXpZ
11 10 rexbii pAp˙WpXpZpAp˙WpXpZ
12 9 11 sylib KHLWHZAZ˙WpAp˙WpXpZ
13 1 2 3 lhpexle2 KHLWHpAp˙WpYpZ
14 3anass p˙WpYpZp˙WpYpZ
15 14 rexbii pAp˙WpYpZpAp˙WpYpZ
16 13 15 sylib KHLWHpAp˙WpYpZ
17 16 3ad2ant1 KHLWHZAZ˙WYAY˙WpAp˙WpYpZ
18 simpl1 KHLWHZAZ˙WYAY˙WXAX˙WKHLWH
19 simpl3l KHLWHZAZ˙WYAY˙WXAX˙WYA
20 simpl2l KHLWHZAZ˙WYAY˙WXAX˙WZA
21 simprl KHLWHZAZ˙WYAY˙WXAX˙WXA
22 simpl3r KHLWHZAZ˙WYAY˙WXAX˙WY˙W
23 simpl2r KHLWHZAZ˙WYAY˙WXAX˙WZ˙W
24 simprr KHLWHZAZ˙WYAY˙WXAX˙WX˙W
25 1 2 3 lhpexle3lem KHLWHYAZAXAY˙WZ˙WX˙WpAp˙WpYpZpX
26 18 19 20 21 22 23 24 25 syl133anc KHLWHZAZ˙WYAY˙WXAX˙WpAp˙WpYpZpX
27 df-3an pYpZpXpYpZpX
28 27 anbi2i p˙WpYpZpXp˙WpYpZpX
29 3anass p˙WpYpZpXp˙WpYpZpX
30 28 29 bitr4i p˙WpYpZpXp˙WpYpZpX
31 30 rexbii pAp˙WpYpZpXpAp˙WpYpZpX
32 26 31 sylib KHLWHZAZ˙WYAY˙WXAX˙WpAp˙WpYpZpX
33 17 32 lhpexle1lem KHLWHZAZ˙WYAY˙WpAp˙WpYpZpX
34 an31 pYpZpXpXpZpY
35 34 anbi2i p˙WpYpZpXp˙WpXpZpY
36 3anass p˙WpXpZpYp˙WpXpZpY
37 35 29 36 3bitr4i p˙WpYpZpXp˙WpXpZpY
38 37 rexbii pAp˙WpYpZpXpAp˙WpXpZpY
39 33 38 sylib KHLWHZAZ˙WYAY˙WpAp˙WpXpZpY
40 39 3expa KHLWHZAZ˙WYAY˙WpAp˙WpXpZpY
41 12 40 lhpexle1lem KHLWHZAZ˙WpAp˙WpXpZpY
42 an32 pXpZpYpXpYpZ
43 42 anbi2i p˙WpXpZpYp˙WpXpYpZ
44 3anass p˙WpXpYpZp˙WpXpYpZ
45 43 36 44 3bitr4i p˙WpXpZpYp˙WpXpYpZ
46 45 rexbii pAp˙WpXpZpYpAp˙WpXpYpZ
47 41 46 sylib KHLWHZAZ˙WpAp˙WpXpYpZ
48 7 47 lhpexle1lem KHLWHpAp˙WpXpYpZ
49 df-3an pXpYpZpXpYpZ
50 49 anbi2i p˙WpXpYpZp˙WpXpYpZ
51 44 50 bitr4i p˙WpXpYpZp˙WpXpYpZ
52 51 rexbii pAp˙WpXpYpZpAp˙WpXpYpZ
53 48 52 sylib KHLWHpAp˙WpXpYpZ